| #
17bc899d |
|
18-Aug-2017 |
wenzelm <none@none> |
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
|
| #
c4a680cf |
|
30-Sep-2016 |
hoelzl <none@none> |
HOL-Analysis: move Continuum_Not_Denumerable from Library
--HG--
rename : src/HOL/Library/Continuum_Not_Denumerable.thy => src/HOL/Analysis/Continuum_Not_Denumerable.thy
|
| #
c054b489 |
|
12-Jul-2016 |
wenzelm <none@none> |
more standard name;
--HG--
rename : src/HOL/Library/ContNotDenum.thy => src/HOL/Library/Continuum_Not_Denumerable.thy
|
| #
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
| #
a2fc4fbf |
|
21-Oct-2014 |
wenzelm <none@none> |
tuned;
|
| #
247ad2f1 |
|
21-Oct-2014 |
wenzelm <none@none> |
update_cartouches;
|
| #
839a96d8 |
|
05-Nov-2013 |
hoelzl <none@none> |
move Lubs from HOL to HOL-Library (replaced by conditionally complete lattices)
--HG--
rename : src/HOL/Library/Glbs.thy => src/HOL/Library/Lubs_Glbs.thy
|
| #
59489bcb |
|
11-Sep-2011 |
wenzelm <none@none> |
misc tuning and clarification;
|
| #
3d40d3d4 |
|
29-Dec-2010 |
wenzelm <none@none> |
explicit file specifications -- avoid secondary load path;
|
| #
079cde2d |
|
17-Oct-2009 |
wenzelm <none@none> |
eliminated hard tabulators, guessing at each author's individual tab-width;
tuned headers;
|
| #
4d6fb612 |
|
24-Jun-2009 |
wenzelm <none@none> |
standard naming conventions for session and theories;
--HG--
rename : src/HOL/HahnBanach/Bounds.thy => src/HOL/Hahn_Banach/Bounds.thy
rename : src/HOL/HahnBanach/FunctionNorm.thy => src/HOL/Hahn_Banach/Function_Norm.thy
rename : src/HOL/HahnBanach/FunctionOrder.thy => src/HOL/Hahn_Banach/Function_Order.thy
rename : src/HOL/HahnBanach/HahnBanach.thy => src/HOL/Hahn_Banach/Hahn_Banach.thy
rename : src/HOL/HahnBanach/HahnBanachExtLemmas.thy => src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy
rename : src/HOL/HahnBanach/HahnBanachLemmas.thy => src/HOL/Hahn_Banach/Hahn_Banach_Lemmas.thy
rename : src/HOL/HahnBanach/HahnBanachSupLemmas.thy => src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy
rename : src/HOL/HahnBanach/Linearform.thy => src/HOL/Hahn_Banach/Linearform.thy
rename : src/HOL/HahnBanach/NormedSpace.thy => src/HOL/Hahn_Banach/Normed_Space.thy
rename : src/HOL/HahnBanach/README.html => src/HOL/Hahn_Banach/README.html
rename : src/HOL/HahnBanach/ROOT.ML => src/HOL/Hahn_Banach/ROOT.ML
rename : src/HOL/HahnBanach/Subspace.thy => src/HOL/Hahn_Banach/Subspace.thy
rename : src/HOL/HahnBanach/VectorSpace.thy => src/HOL/Hahn_Banach/Vector_Space.thy
rename : src/HOL/HahnBanach/ZornLemma.thy => src/HOL/Hahn_Banach/Zorn_Lemma.thy
rename : src/HOL/HahnBanach/document/root.bib => src/HOL/Hahn_Banach/document/root.bib
rename : src/HOL/HahnBanach/document/root.tex => src/HOL/Hahn_Banach/document/root.tex
|