2010-04-23 wenzelm [Fri, 23 Apr 2010 23:35:43 +0200] rev 36319
mark schematic statements explicitly;
src/CCL/Fix.thy src/CCL/Wfd.thy src/CTT/Arith.thy src/CTT/ex/Elimination.thy src/CTT/ex/Synthesis.thy src/CTT/ex/Typechecking.thy src/Cube/Example.thy src/FOL/ex/Classical.thy src/FOL/ex/Prolog.thy src/FOL/ex/Quantifiers_Cla.thy src/FOL/ex/Quantifiers_Int.thy src/FOLP/FOLP.thy src/FOLP/IFOLP.thy src/FOLP/ex/Classical.thy src/FOLP/ex/Foundation.thy src/FOLP/ex/If.thy src/FOLP/ex/Intro.thy src/FOLP/ex/Intuitionistic.thy src/FOLP/ex/Nat.thy src/FOLP/ex/Propositional_Cla.thy src/FOLP/ex/Propositional_Int.thy src/FOLP/ex/Quantifiers_Cla.thy src/FOLP/ex/Quantifiers_Int.thy src/HOL/Bali/Example.thy src/HOL/Lambda/Type.thy src/HOL/MicroJava/J/Example.thy src/HOL/Nitpick_Examples/Core_Nits.thy src/HOL/Nitpick_Examples/Refute_Nits.thy src/HOL/Prolog/Func.thy src/HOL/Prolog/Test.thy src/HOL/Prolog/Type.thy src/HOL/ex/Classical.thy src/HOL/ex/Groebner_Examples.thy src/HOL/ex/Refute_Examples.thy src/HOL/ex/set.thy src/Sequents/LK/Quantifiers.thy src/ZF/AC/Cardinal_aux.thy src/ZF/Constructible/Reflection.thy

2010-04-23 wenzelm [Fri, 23 Apr 2010 23:33:48 +0200] rev 36318
eliminated spurious schematic statements;
src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy src/HOL/Multivariate_Analysis/Integration.thy

2010-04-23 wenzelm [Fri, 23 Apr 2010 22:48:07 +0200] rev 36317
explicit 'schematic_theorem' etc. for schematic theorem statements;
NEWS src/Pure/Isar/isar_syn.ML src/Pure/Isar/specification.ML

2010-04-23 wenzelm [Fri, 23 Apr 2010 22:39:49 +0200] rev 36316
collapse category "schematic goal" in keyword table -- Proof General does not know about this;
lib/scripts/keywords

2010-04-23 wenzelm [Fri, 23 Apr 2010 21:00:28 +0200] rev 36315
added keyword category "schematic goal", which prevents any attempt to fork the proof;
src/Pure/Isar/outer_keyword.ML src/Pure/Isar/toplevel.ML src/Pure/ProofGeneral/pgip_parser.ML

2010-04-23 wenzelm [Fri, 23 Apr 2010 19:36:23 +0200] rev 36314
merged
src/HOL/Tools/Sledgehammer/named_thm_set.ML

2010-04-23 haftmann [Fri, 23 Apr 2010 19:32:37 +0200] rev 36313
merged

2010-04-23 haftmann [Fri, 23 Apr 2010 16:45:53 +0200] rev 36312
separated instantiation of division_by_zero
src/HOL/Library/Fraction_Field.thy

2010-04-23 haftmann [Fri, 23 Apr 2010 16:38:51 +0200] rev 36311
epheremal replacement of field_simps by field_eq_simps; dropped old division_by_zero instance
src/HOL/Library/Formal_Power_Series.thy

2010-04-23 haftmann [Fri, 23 Apr 2010 16:17:25 +0200] rev 36310
adapted to new times_divide_eq simp situation
src/HOL/NSA/HDeriv.thy