2008-11-03 haftmann [Mon, 03 Nov 2008 14:15:25 +0100] rev 28714
improved verbatim mechanism
doc-src/IsarAdvanced/Classes/IsaMakefile doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex doc-src/IsarAdvanced/Classes/classes.tex doc-src/IsarAdvanced/Codegen/Thy/Adaption.thy doc-src/IsarAdvanced/Codegen/Thy/document/Adaption.tex doc-src/IsarAdvanced/Codegen/Thy/document/Introduction.tex doc-src/IsarAdvanced/Codegen/Thy/document/Program.tex doc-src/IsarAdvanced/Codegen/codegen.tex doc-src/more_antiquote.ML

2008-10-31 berghofe [Fri, 31 Oct 2008 10:39:04 +0100] rev 28713
Theorem "_" is now stored with open derivation.
src/Pure/drule.ML

2008-10-31 berghofe [Fri, 31 Oct 2008 10:37:34 +0100] rev 28712
Removed argument prf2 in rewrite rules for equal_elim to make them applicable
to eta-contracted proofs.
src/HOL/Tools/rewrite_hol_proof.ML

2008-10-31 berghofe [Fri, 31 Oct 2008 10:35:30 +0100] rev 28711
Replaced arbitrary by undefined.
src/HOL/Fun.thy

2008-10-30 ballarin [Thu, 30 Oct 2008 10:57:45 +0100] rev 28710
Dropped context element 'includes'.
NEWS src/Pure/Isar/locale.ML src/Pure/Isar/spec_parse.ML src/Pure/Isar/specification.ML

2008-10-29 haftmann [Wed, 29 Oct 2008 15:32:58 +0100] rev 28709
adapted to strict pattern discipline
src/HOL/ex/NormalForm.thy

2008-10-29 haftmann [Wed, 29 Oct 2008 11:33:40 +0100] rev 28708
explicit check for pattern discipline before code translation
src/HOL/Library/Code_Index.thy src/HOL/Library/Multiset.thy src/HOL/List.thy src/HOL/Tools/numeral.ML src/Pure/Isar/code.ML src/Pure/Isar/code_unit.ML src/Tools/code/code_haskell.ML src/Tools/code/code_ml.ML src/Tools/code/code_printer.ML src/Tools/code/code_thingol.ML

2008-10-28 ballarin [Tue, 28 Oct 2008 17:53:46 +0100] rev 28707
Revoked workaround (incompatible with HOL/ex/LocaleTest2.thy).
src/Pure/Isar/theory_target.ML

2008-10-28 haftmann [Tue, 28 Oct 2008 16:59:02 +0100] rev 28706
restored incremental code generation
src/Tools/code/code_thingol.ML src/Tools/nbe.ML

2008-10-28 haftmann [Tue, 28 Oct 2008 16:59:01 +0100] rev 28705
slightly tuned
src/Tools/code/code_ml.ML