2009-07-16 wenzelm [Thu, 16 Jul 2009 00:24:11 +0200] rev 32014
removed obsolete/unused legacy_varify;
src/Pure/logic.ML

2009-07-16 wenzelm [Thu, 16 Jul 2009 00:21:36 +0200] rev 32013
eliminated legacy_varify;
src/HOL/Tools/Datatype/datatype_realizer.ML

2009-07-15 wenzelm [Wed, 15 Jul 2009 23:50:40 +0200] rev 32012
merged

2009-07-15 Christian Urban <urbanc@in.tum.de> [Wed, 15 Jul 2009 22:30:27 +0200] rev 32011
simplified proofs
src/HOL/Nominal/Examples/Fsub.thy

2009-07-15 wenzelm [Wed, 15 Jul 2009 23:48:21 +0200] rev 32010
more antiquotations;
src/CCL/CCL.thy src/CCL/Hered.thy src/CCL/Term.thy src/CCL/Type.thy src/FOL/simpdata.ML src/HOL/Algebra/abstract/Ring2.thy src/HOL/Divides.thy src/HOL/IntDiv.thy src/HOL/Lambda/WeakNorm.thy src/HOL/List.thy src/HOL/Modelcheck/EindhovenSyn.thy src/HOL/Modelcheck/MuckeSyn.thy src/HOL/Nominal/nominal_datatype.ML src/HOL/Nominal/nominal_permeq.ML src/HOL/OrderedGroup.thy src/HOL/Product_Type.thy src/HOL/Prolog/prolog.ML src/HOL/Set.thy src/HOL/Statespace/DistinctTreeProver.thy src/HOL/Statespace/state_fun.ML src/HOL/Tools/metis_tools.ML src/HOL/Tools/nat_arith.ML src/HOL/Tools/nat_numeral_simprocs.ML src/HOL/Tools/numeral.ML src/HOL/Tools/res_axioms.ML src/HOL/Tools/rewrite_hol_proof.ML src/HOL/Tools/sat_funcs.ML src/HOL/Tools/simpdata.ML src/HOLCF/holcf_logic.ML src/ZF/Datatype_ZF.thy src/ZF/OrdQuant.thy

2009-07-15 wenzelm [Wed, 15 Jul 2009 23:11:57 +0200] rev 32009
eliminated obsolete legacy_varify;
src/Pure/Isar/theory_target.ML

2009-07-15 wenzelm [Wed, 15 Jul 2009 21:42:24 +0200] rev 32008
tuned comment;
src/Pure/logic.ML

2009-07-15 nipkow [Wed, 15 Jul 2009 20:34:58 +0200] rev 32007
Made "prime" executable
src/HOL/GCD.thy src/HOL/List.thy

2009-07-15 nipkow [Wed, 15 Jul 2009 15:09:33 +0200] rev 32006
More finite set induction rules
src/HOL/Finite_Set.thy src/HOL/SetInterval.thy

2009-07-15 nipkow [Wed, 15 Jul 2009 12:44:41 +0200] rev 32005
made upt/upto executable on nat/int by simp
src/HOL/List.thy