2008-06-10 haftmann [Tue, 10 Jun 2008 15:31:01 +0200] rev 27109
more instantiation
src/HOL/Library/ListVector.thy

2008-06-10 haftmann [Tue, 10 Jun 2008 15:30:59 +0200] rev 27108
whitespace tuning
src/HOL/Auth/Guard/GuardK.thy src/HOL/Complex/Fundamental_Theorem_Algebra.thy src/HOL/Hyperreal/Series.thy src/HOLCF/ex/Dnat.thy

2008-06-10 haftmann [Tue, 10 Jun 2008 15:30:58 +0200] rev 27107
localized Least in Orderings.thy
src/HOL/HOL.thy src/HOL/Orderings.thy

2008-06-10 haftmann [Tue, 10 Jun 2008 15:30:56 +0200] rev 27106
removed some dubious code lemmas
src/HOL/Fun.thy src/HOL/Int.thy src/HOL/Library/GCD.thy src/HOL/Library/Multiset.thy src/HOL/Library/Primes.thy src/HOL/Library/Word.thy src/HOL/List.thy src/HOL/Real/PReal.thy src/HOL/Real/RealDef.thy src/HOL/Set.thy

2008-06-10 haftmann [Tue, 10 Jun 2008 15:30:54 +0200] rev 27105
slightly tuning of some proofs involving case distinction and induction on natural numbers and similar
src/HOL/Algebra/Exponent.thy src/HOL/Auth/Message.thy src/HOL/Complex/CLim.thy src/HOL/Hyperreal/HyperDef.thy src/HOL/Hyperreal/HyperNat.thy src/HOL/Word/BinBoolList.thy src/HOLCF/IOA/meta_theory/Sequence.thy

2008-06-10 haftmann [Tue, 10 Jun 2008 15:30:33 +0200] rev 27104
rep_datatype command now takes list of constructors as input arguments
NEWS src/HOL/Datatype.thy src/HOL/HoareParallel/OG_Tactics.thy src/HOL/Library/Code_Index.thy src/HOL/MetisExamples/BT.thy src/HOL/Nat.thy src/HOL/Product_Type.thy src/HOL/Sum_Type.thy src/HOL/TLA/Action.thy src/HOL/Tools/datatype_package.ML src/HOL/Tools/record_package.ML src/HOLCF/Lift.thy

2008-06-10 haftmann [Tue, 10 Jun 2008 15:30:06 +0200] rev 27103
major refactorings in code generator modules
doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy doc-src/IsarRef/Thy/HOL_Specific.thy doc-src/IsarRef/Thy/document/HOL_Specific.tex lib/Tools/codegen src/HOL/Code_Setup.thy src/HOL/IsaMakefile src/HOL/Library/Eval.thy src/HOL/Library/Eval_Witness.thy src/HOL/ex/ExecutableContent.thy src/HOL/ex/Quickcheck.thy src/Tools/code/code_funcgr.ML src/Tools/code/code_name.ML src/Tools/code/code_package.ML src/Tools/code/code_target.ML src/Tools/code/code_thingol.ML src/Tools/nbe.ML

2008-06-10 haftmann [Tue, 10 Jun 2008 15:30:01 +0200] rev 27102
updated
etc/isar-keywords.el lib/jedit/isabelle.xml

2008-06-10 haftmann [Tue, 10 Jun 2008 14:32:58 +0200] rev 27101
slightly tuning of some proofs involving case distinction and induction on natural numbers and similar
src/HOLCF/FOCUS/Buffer_adm.thy src/HOLCF/FOCUS/Stream_adm.thy

2008-06-09 wenzelm [Mon, 09 Jun 2008 17:39:35 +0200] rev 27100
DatatypePackage.case_tac;
src/HOL/TLA/Memory/MemoryImplementation.thy