2007-08-09 haftmann [Thu, 09 Aug 2007 15:52:54 +0200] rev 24199
new access interface in defs.ML
src/Pure/defs.ML src/Pure/theory.ML

2007-08-09 haftmann [Thu, 09 Aug 2007 15:52:53 +0200] rev 24198
adaptions for code generation
src/HOL/Real/Rational.thy src/HOL/Real/RealDef.thy

2007-08-09 haftmann [Thu, 09 Aug 2007 15:52:49 +0200] rev 24197
proper implementation of rational numbers
src/HOL/Library/Abstract_Rat.thy src/HOL/Library/Executable_Rat.thy src/HOL/Library/Executable_Real.thy src/HOL/Library/Library.thy src/HOL/ex/ExecutableContent.thy

2007-08-09 haftmann [Thu, 09 Aug 2007 15:52:47 +0200] rev 24196
localized of_nat
src/HOL/IntDef.thy src/HOL/Nat.thy src/HOL/Real/rat_arith.ML src/HOL/Tools/lin_arith.ML src/HOL/int_arith1.ML

2007-08-09 haftmann [Thu, 09 Aug 2007 15:52:45 +0200] rev 24195
tuned
src/HOL/Hyperreal/StarClasses.thy src/HOL/IntArith.thy src/HOL/IntDiv.thy src/HOL/Library/Efficient_Nat.thy src/HOL/Library/State_Monad.thy src/HOL/Tools/ATP/reduce_axiomsN.ML src/HOL/ex/Codegenerator.thy src/HOL/ex/Codegenerator_Pretty.thy src/HOL/ex/ROOT.ML src/Pure/Tools/codegen_thingol.ML

2007-08-09 haftmann [Thu, 09 Aug 2007 15:52:42 +0200] rev 24194
re-eliminated Option.thy
src/HOL/Bali/Basis.thy src/HOL/Bali/Table.thy src/HOL/Datatype.thy src/HOL/Extraction.thy src/HOL/Finite_Set.thy src/HOL/FunDef.thy src/HOL/IsaMakefile src/HOL/Nominal/nominal_atoms.ML src/HOL/Option.thy

2007-08-09 haftmann [Thu, 09 Aug 2007 15:52:38 +0200] rev 24193
updated
doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex doc-src/IsarAdvanced/Codegen/Thy/examples/fac_case.ML doc-src/IsarAdvanced/Codegen/Thy/examples/lexicographic.ML doc-src/IsarAdvanced/Codegen/Thy/examples/monotype.ML doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML doc-src/IsarAdvanced/Codegen/Thy/examples/tree.ML doc-src/manual.bib

2007-08-09 aspinall [Thu, 09 Aug 2007 11:39:29 +0200] rev 24192
PGIP change: thyname is optional in opentheory, markup even in case of header parse failure
src/Pure/ProofGeneral/parsing.ML src/Pure/ProofGeneral/pgip_markup.ML src/Pure/ProofGeneral/pgip_parser.ML src/Pure/ProofGeneral/pgip_tests.ML

2007-08-09 aspinall [Thu, 09 Aug 2007 11:37:27 +0200] rev 24191
Typo in comment
src/Pure/ProofGeneral/preferences.ML

2007-08-08 wenzelm [Wed, 08 Aug 2007 23:07:50 +0200] rev 24190
discontinued attached ML files;
end_theory: fail on unresolved dependencies;
src/Pure/Thy/thy_info.ML