2010-02-13 wenzelm [Sat, 13 Feb 2010 23:24:57 +0100] rev 35123
modernized structures;
src/HOL/Int.thy src/HOL/RealPow.thy src/HOL/String.thy src/HOL/Tools/float_syntax.ML src/HOL/Tools/numeral_syntax.ML src/HOL/Tools/string_syntax.ML src/ZF/Bin.thy src/ZF/Tools/numeral_syntax.ML src/ZF/int_arith.ML

2010-02-13 wenzelm [Sat, 13 Feb 2010 23:16:06 +0100] rev 35122
authentic proof syntax;
src/Pure/Proof/proof_syntax.ML

2010-02-12 haftmann [Fri, 12 Feb 2010 14:28:01 +0100] rev 35121
tuned import order
src/HOL/Lattices.thy src/HOL/Nat.thy

2010-02-12 haftmann [Fri, 12 Feb 2010 09:49:28 +0100] rev 35120
tuned comments
src/Pure/Isar/class.ML

2010-02-11 wenzelm [Thu, 11 Feb 2010 23:50:38 +0100] rev 35119
merged

2010-02-11 huffman [Thu, 11 Feb 2010 12:26:50 -0800] rev 35118
merged
src/HOL/Library/Quotient.thy src/HOL/Library/Structure_Syntax.thy

2010-02-11 huffman [Thu, 11 Feb 2010 12:26:07 -0800] rev 35117
change generated lemmas dist_eqs and dist_les to iff-style
src/HOLCF/Domain.thy src/HOLCF/IOA/meta_theory/Sequence.thy src/HOLCF/Tools/Domain/domain_theorems.ML

2010-02-11 boehmes [Thu, 11 Feb 2010 17:48:55 +0100] rev 35116
unfold quantifiers (Ball, Bex, Ex1)
src/HOL/SMT/Tools/smt_normalize.ML

2010-02-11 wenzelm [Thu, 11 Feb 2010 23:00:22 +0100] rev 35115
modernized translations;
formal markup of @{syntax_const} and @{const_syntax};
minor tuning;
src/HOL/Complete_Lattice.thy src/HOL/Finite_Set.thy src/HOL/Fun.thy src/HOL/HOL.thy src/HOL/Hilbert_Choice.thy src/HOL/Inductive.thy src/HOL/Library/Coinductive_List.thy src/HOL/Library/Numeral_Type.thy src/HOL/Library/OptionalSugar.thy src/HOL/Library/State_Monad.thy src/HOL/List.thy src/HOL/Map.thy src/HOL/Orderings.thy src/HOL/Product_Type.thy src/HOL/Set.thy src/HOL/SetInterval.thy src/HOL/String.thy src/HOL/Tools/float_syntax.ML src/HOL/Tools/numeral_syntax.ML src/HOL/Tools/string_syntax.ML src/HOL/Typerep.thy src/HOLCF/Cfun.thy src/HOLCF/Fixrec.thy src/HOLCF/Sprod.thy

2010-02-11 wenzelm [Thu, 11 Feb 2010 22:55:16 +0100] rev 35114
formal markup of @{syntax_const} and @{const_syntax};
authentic syntax for extra robustness;
src/HOL/Statespace/StateFun.thy src/HOL/Statespace/StateSpaceSyntax.thy