2008-10-24 haftmann [Fri, 24 Oct 2008 17:48:39 +0200] rev 28686
tuned
src/HOL/ex/Codegenerator.thy

2008-10-24 haftmann [Fri, 24 Oct 2008 17:48:37 +0200] rev 28685
new classes "top" and "bot"
NEWS src/HOL/Lattices.thy src/HOL/Orderings.thy src/HOL/SizeChange/Graphs.thy

2008-10-24 haftmann [Fri, 24 Oct 2008 17:48:36 +0200] rev 28684
tuned proof
src/HOL/Library/Enum.thy

2008-10-24 haftmann [Fri, 24 Oct 2008 17:48:35 +0200] rev 28683
more clever module name aliasses for code generation
src/HOL/Library/Efficient_Nat.thy

2008-10-24 haftmann [Fri, 24 Oct 2008 17:48:34 +0200] rev 28682
"arbitrary" merely abbreviates undefined
src/HOL/HOL.thy

2008-10-24 haftmann [Fri, 24 Oct 2008 17:48:33 +0200] rev 28681
subst is a proper axiom again
src/FOL/IFOL.thy

2008-10-24 haftmann [Fri, 24 Oct 2008 10:41:15 +0200] rev 28680
updated
doc-src/IsarAdvanced/Codegen/Thy/document/ML.tex

2008-10-24 haftmann [Fri, 24 Oct 2008 10:41:13 +0200] rev 28679
explicit namings for generated code
doc-src/IsarAdvanced/Codegen/Thy/Adaption.thy doc-src/IsarAdvanced/Codegen/Thy/document/Adaption.tex doc-src/more_antiquote.ML

2008-10-23 wenzelm [Thu, 23 Oct 2008 16:07:03 +0200] rev 28678
Thm.get_def;
src/ZF/Tools/datatype_package.ML src/ZF/Tools/inductive_package.ML

2008-10-23 wenzelm [Thu, 23 Oct 2008 15:28:39 +0200] rev 28677
Thm.def_name;
src/HOL/Import/hol4rews.ML src/HOL/Import/proof_kernel.ML