2015-11-13 paulson <lp15@cam.ac.uk> [Fri, 13 Nov 2015 12:27:13 +0000] rev 61649
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
src/HOL/Archimedean_Field.thy src/HOL/Binomial.thy src/HOL/Complex.thy src/HOL/Decision_Procs/Approximation.thy src/HOL/Decision_Procs/MIR.thy src/HOL/Divides.thy src/HOL/GCD.thy src/HOL/Inequalities.thy src/HOL/Int.thy src/HOL/Library/Float.thy src/HOL/Library/Formal_Power_Series.thy src/HOL/Library/Numeral_Type.thy src/HOL/Limits.thy src/HOL/Multivariate_Analysis/Complex_Transcendental.thy src/HOL/Multivariate_Analysis/Derivative.thy src/HOL/Multivariate_Analysis/Integration.thy src/HOL/NSA/NSA.thy src/HOL/Nat.thy src/HOL/Nat_Transfer.thy src/HOL/NthRoot.thy src/HOL/Number_Theory/Fib.thy src/HOL/Old_Number_Theory/Euler.thy src/HOL/Old_Number_Theory/EvenOdd.thy src/HOL/Old_Number_Theory/WilsonRuss.thy src/HOL/Power.thy src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy src/HOL/Real.thy src/HOL/Real_Vector_Spaces.thy src/HOL/Rings.thy src/HOL/Transcendental.thy src/HOL/Word/Word.thy src/HOL/ex/Sqrt.thy src/HOL/ex/Sum_of_Powers.thy src/HOL/ex/Transfer_Int_Nat.thy

2015-11-13 nipkow [Fri, 13 Nov 2015 12:28:11 +0100] rev 61648
tuned name
src/HOL/Data_Structures/AVL_Map.thy

2015-11-13 nipkow [Fri, 13 Nov 2015 12:06:50 +0100] rev 61647
tuned
src/HOL/Data_Structures/AVL_Set.thy src/HOL/Data_Structures/Tree_Map.thy src/HOL/Data_Structures/Tree_Set.thy

2015-11-12 blanchet [Thu, 12 Nov 2015 21:12:09 +0100] rev 61646
use cartouches instead of backquotes
src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML

2015-11-12 nipkow [Thu, 12 Nov 2015 13:50:54 +0100] rev 61645
translation for conjunctive premises
src/Doc/Sugar/Sugar.thy src/HOL/Library/OptionalSugar.thy

2015-11-12 nipkow [Thu, 12 Nov 2015 11:22:26 +0100] rev 61644
tuned
src/Doc/Prog_Prove/Basics.thy

2015-11-12 nipkow [Thu, 12 Nov 2015 11:05:38 +0100] rev 61643
added proof state output warning
src/Doc/Prog_Prove/Basics.thy

2015-11-11 nipkow [Wed, 11 Nov 2015 19:22:18 +0100] rev 61642
tuned
src/HOL/Data_Structures/List_Ins_Del.thy

2015-11-11 nipkow [Wed, 11 Nov 2015 18:32:36 +0100] rev 61641
merged

2015-11-11 nipkow [Wed, 11 Nov 2015 18:32:26 +0100] rev 61640
no CRLF
src/HOL/Data_Structures/AList_Upd_Del.thy src/HOL/Data_Structures/Cmp.thy src/HOL/Data_Structures/Less_False.thy src/HOL/Data_Structures/List_Ins_Del.thy src/HOL/Data_Structures/Map_by_Ordered.thy src/HOL/Data_Structures/Set_by_Ordered.thy src/HOL/Data_Structures/Sorted_Less.thy src/HOL/Data_Structures/Tree23.thy src/HOL/Data_Structures/Tree234.thy src/HOL/Data_Structures/Tree234_Map.thy src/HOL/Data_Structures/Tree234_Set.thy src/HOL/Data_Structures/Tree23_Map.thy src/HOL/Data_Structures/Tree23_Set.thy src/HOL/Data_Structures/Tree_Map.thy src/HOL/Data_Structures/Tree_Set.thy