2011-04-23 wenzelm [Sat, 23 Apr 2011 13:53:09 +0200] rev 42464
proper binding/report of defined simprocs;
tuned signature;
src/Pure/Isar/args.ML src/Pure/Isar/isar_cmd.ML src/Pure/Isar/isar_syn.ML src/Pure/simplifier.ML

2011-04-23 wenzelm [Sat, 23 Apr 2011 13:00:19 +0200] rev 42463
modernized specifications;
src/HOL/Imperative_HOL/Heap.thy src/HOL/Imperative_HOL/ex/SatChecker.thy src/HOL/Library/Abstract_Rat.thy src/HOL/Matrix/Matrix.thy src/HOL/Matrix/SparseMatrix.thy src/HOL/Metis_Examples/Message.thy src/HOL/MicroJava/BV/Effect.thy src/HOL/MicroJava/BV/JVMType.thy src/HOL/MicroJava/BV/LBVJVM.thy src/HOL/MicroJava/DFA/Err.thy src/HOL/MicroJava/DFA/LBVSpec.thy src/HOL/MicroJava/DFA/Semilat.thy src/HOL/MicroJava/DFA/Typing_Framework.thy src/HOL/MicroJava/J/Conform.thy src/HOL/MicroJava/J/Decl.thy src/HOL/MicroJava/J/State.thy src/HOL/MicroJava/J/WellForm.thy src/HOL/MicroJava/J/WellType.thy src/HOL/MicroJava/JVM/JVMInstructions.thy src/HOL/MicroJava/JVM/JVMState.thy src/HOL/NSA/HyperDef.thy src/HOL/NSA/HyperNat.thy src/HOL/NSA/NSComplex.thy src/HOL/NanoJava/AxSem.thy src/HOL/NanoJava/Decl.thy src/HOL/NanoJava/State.thy src/HOL/Nitpick_Examples/Hotel_Nits.thy src/HOL/Predicate_Compile_Examples/Examples.thy src/HOL/Predicate_Compile_Examples/Hotel_Example.thy src/HOL/Predicate_Compile_Examples/IMP_4.thy src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy src/HOL/SET_Protocol/Message_SET.thy src/HOL/UNITY/Comp/Client.thy src/HOL/UNITY/Comp/Counter.thy src/HOL/UNITY/Comp/Counterc.thy src/HOL/UNITY/Comp/Priority.thy src/HOL/UNITY/Comp/TimerArray.thy src/HOL/UNITY/Simple/Channel.thy src/HOL/UNITY/Simple/Mutex.thy src/HOL/UNITY/Simple/NSP_Bad.thy src/HOL/UNITY/Simple/Network.thy src/HOL/UNITY/Simple/Reach.thy src/HOL/UNITY/Simple/Reachability.thy src/HOL/Word/Examples/WordExamples.thy src/HOL/ex/CTL.thy src/HOL/ex/Groebner_Examples.thy src/HOL/ex/RPred.thy src/HOL/ex/Records.thy ...

2011-04-22 wenzelm [Fri, 22 Apr 2011 15:57:43 +0200] rev 42462
tuned signature;
src/Provers/Arith/cancel_numerals.ML

2011-04-22 wenzelm [Fri, 22 Apr 2011 15:25:01 +0200] rev 42461
stats for mac-poly-M2;
Admin/isatest/isatest-stats

2011-04-22 wenzelm [Fri, 22 Apr 2011 15:24:00 +0200] rev 42460
simplified Data signature;
src/FOL/simpdata.ML src/HOL/Tools/simpdata.ML src/Provers/quantifier1.ML

2011-04-22 wenzelm [Fri, 22 Apr 2011 15:05:04 +0200] rev 42459
misc tuning and simplification;
src/FOL/FOL.thy src/HOL/HOL.thy src/HOL/Set.thy src/Provers/quantifier1.ML src/ZF/OrdQuant.thy src/ZF/pair.thy

2011-04-22 wenzelm [Fri, 22 Apr 2011 14:53:11 +0200] rev 42458
misc tuning;
src/FOL/simpdata.ML src/HOL/Tools/simpdata.ML src/Provers/quantifier1.ML

2011-04-22 wenzelm [Fri, 22 Apr 2011 14:38:49 +0200] rev 42457
do not open ML structures;
src/Provers/quantifier1.ML

2011-04-22 wenzelm [Fri, 22 Apr 2011 14:30:32 +0200] rev 42456
proper context for Quantifier1 simprocs (avoid bad ProofContext.init_global from abc655166d61);
tuned signature;
src/FOL/FOL.thy src/HOL/HOL.thy src/HOL/Set.thy src/Provers/quantifier1.ML src/ZF/OrdQuant.thy src/ZF/pair.thy

2011-04-22 wenzelm [Fri, 22 Apr 2011 13:58:13 +0200] rev 42455
modernized Quantifier1 simproc setup;
src/FOL/FOL.thy src/FOL/simpdata.ML src/HOL/HOL.thy src/HOL/Set.thy src/HOL/Tools/Meson/meson.ML src/HOL/Tools/simpdata.ML src/ZF/OrdQuant.thy src/ZF/pair.thy src/ZF/simpdata.ML