2008-04-03 berghofe [Thu, 03 Apr 2008 18:13:50 +0200] rev 26536
Added skip_mono flag to inductive definition package.
src/HOL/Nominal/nominal_package.ML

2008-04-03 berghofe [Thu, 03 Apr 2008 17:55:12 +0200] rev 26535
Added skip_mono flag to inductive definition package.
src/HOL/Tools/function_package/inductive_wrap.ML src/HOL/Tools/inductive_realizer.ML

2008-04-03 berghofe [Thu, 03 Apr 2008 17:54:19 +0200] rev 26534
Added skip_mono flag and inductive_flags type.
src/HOL/Tools/inductive_package.ML src/HOL/Tools/inductive_set_package.ML

2008-04-03 berghofe [Thu, 03 Apr 2008 17:52:51 +0200] rev 26533
Deleted code for axiomatic introduction of datatypes. Instead, the package
now uses SkipProof.prove rather than Goal.prove to do proofs.
src/HOL/Tools/datatype_package.ML

2008-04-03 berghofe [Thu, 03 Apr 2008 17:50:50 +0200] rev 26532
Removed QuickAndDirty constructor from simproc_dist datatype.
src/HOL/Tools/datatype_aux.ML

2008-04-03 berghofe [Thu, 03 Apr 2008 17:49:39 +0200] rev 26531
- use SkipProof.prove_global instead of Goal.prove_global
- added skip_mono flag to inductive definition package
src/HOL/Tools/datatype_abs_proofs.ML src/HOL/Tools/datatype_rep_proofs.ML

2008-04-03 berghofe [Thu, 03 Apr 2008 17:43:01 +0200] rev 26530
Added prove_global.
src/Pure/Isar/skip_proof.ML

2008-04-03 krauss [Thu, 03 Apr 2008 16:34:52 +0200] rev 26529
Function package no longer overwrites theorems.
Some tuning.
src/HOL/Tools/function_package/context_tree.ML src/HOL/Tools/function_package/fundef_common.ML src/HOL/Tools/function_package/fundef_core.ML src/HOL/Tools/function_package/fundef_package.ML src/HOL/Tools/function_package/lexicographic_order.ML src/HOL/Tools/function_package/mutual.ML

2008-04-03 wenzelm [Thu, 03 Apr 2008 16:03:59 +0200] rev 26528
Why XML notation?
src/Pure/General/yxml.ML

2008-04-03 wenzelm [Thu, 03 Apr 2008 16:03:57 +0200] rev 26527
Symbol.STX, Symbol.DEL;
src/Pure/Tools/isabelle_process.ML