#
a2bc0021 |
|
25-Apr-2016 |
wenzelm <none@none> |
eliminated old 'def'; tuned comments;
|
#
7b34923e |
|
20-Dec-2015 |
wenzelm <none@none> |
tuned whitespace;
|
#
0163a451 |
|
02-Nov-2015 |
wenzelm <none@none> |
tuned document;
|
#
cb1b7551 |
|
02-Nov-2015 |
wenzelm <none@none> |
isabelle update_cartouches -t;
|
#
5da9f3bd |
|
19-Oct-2015 |
wenzelm <none@none> |
tuned document;
|
#
621b6c41 |
|
13-Jun-2015 |
wenzelm <none@none> |
tuned proofs;
|
#
8acf1ce1 |
|
13-Nov-2014 |
wenzelm <none@none> |
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style; discontinued obsolete 'txt_raw' (superseded by 'text_raw'); eliminated obsolete Outer_Syntax.markup (superseded by keyword kinds); 'text' and 'txt' no longer appear in Sidekick tree due to change of keyword kind; changed tagging of diagnostic commands within proof;
|
#
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
#
247ad2f1 |
|
21-Oct-2014 |
wenzelm <none@none> |
update_cartouches;
|
#
d9333ba5 |
|
19-Oct-2012 |
webertj <none@none> |
Renamed {left,right}_distrib to distrib_{right,left}.
|
#
87aca2ae |
|
12-Apr-2012 |
krauss <none@none> |
Set_Algebras: removed syntax \<oplus> and \<otimes>, in favour of plain + and *
|
#
c474d5d8 |
|
13-Aug-2011 |
huffman <none@none> |
HOL-Hahn_Banach: use Set_Algebras library
|
#
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
|