2009-10-20 haftmann [Tue, 20 Oct 2009 16:13:01 +0200] rev 33037
replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
NEWS src/HOL/Import/proof_kernel.ML src/HOL/Import/shuffler.ML src/HOL/Nominal/nominal_primrec.ML src/HOL/Set.thy src/HOL/Tools/Datatype/datatype.ML src/HOL/Tools/Datatype/datatype_aux.ML src/HOL/Tools/Function/context_tree.ML src/HOL/Tools/Function/pattern_split.ML src/HOL/Tools/Groebner_Basis/groebner.ML src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML src/HOL/Tools/Qelim/cooper.ML src/HOL/Tools/inductive_codegen.ML src/HOL/Tools/inductive_set.ML src/HOL/Tools/metis_tools.ML src/HOL/Tools/old_primrec.ML src/HOL/Tools/primrec.ML src/HOL/Tools/prop_logic.ML src/HOL/Tools/record.ML src/HOL/Tools/refute.ML src/HOL/Tools/res_atp.ML src/HOL/Tools/res_clause.ML src/HOL/Tools/res_hol_clause.ML src/HOL/Tools/res_reconstruct.ML src/HOL/Tools/sat_solver.ML src/HOL/Tools/transfer.ML src/HOL/ex/predicate_compile.ML src/HOLCF/Tools/Domain/domain_extender.ML src/Provers/Arith/cancel_div_mod.ML src/Provers/Arith/fast_lin_arith.ML src/Pure/General/name_space.ML src/Pure/General/ord_list.ML src/Pure/General/path.ML src/Pure/Proof/reconstruct.ML src/Pure/ProofGeneral/pgip_parser.ML src/Pure/Syntax/ast.ML src/Pure/Syntax/parser.ML src/Pure/Syntax/syn_ext.ML src/Pure/Tools/find_theorems.ML src/Pure/codegen.ML src/Pure/library.ML src/Pure/meta_simplifier.ML src/Pure/pattern.ML src/Pure/proofterm.ML src/Pure/sorts.ML src/Pure/thm.ML src/Pure/variable.ML src/Tools/IsaPlanner/rw_inst.ML src/Tools/Metis/metis_env.ML src/ZF/Tools/primrec_package.ML

2009-10-21 kleing [Wed, 21 Oct 2009 16:41:22 +1100] rev 33036
find_theorems: better handling of abbreviations (by Timothy Bourke)
src/Pure/Tools/find_theorems.ML

2009-10-21 wenzelm [Wed, 21 Oct 2009 00:36:12 +0200] rev 33035
standardized basic operations on type option;
src/HOL/Import/proof_kernel.ML src/HOL/Import/replay.ML src/HOL/Library/Numeral_Type.thy src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML src/HOL/Library/normarith.ML src/HOL/Library/positivstellensatz.ML src/HOL/Modelcheck/MuckeSyn.thy src/HOL/Nominal/nominal_datatype.ML src/HOL/Tools/Datatype/datatype_codegen.ML src/HOL/Tools/Datatype/datatype_realizer.ML src/HOL/Tools/Groebner_Basis/groebner.ML src/HOL/Tools/Qelim/cooper.ML src/HOL/Tools/Qelim/langford.ML src/HOL/Tools/TFL/rules.ML src/HOL/Tools/TFL/tfl.ML src/HOL/Tools/cnf_funcs.ML src/HOL/Tools/lin_arith.ML src/HOL/Tools/metis_tools.ML src/HOL/Tools/refute.ML src/HOL/Tools/res_atp.ML src/HOL/Tools/res_hol_clause.ML src/HOL/Tools/res_reconstruct.ML src/HOL/Tools/sat_funcs.ML src/HOL/Tools/sat_solver.ML src/Pure/ProofGeneral/pgip_output.ML src/Pure/ProofGeneral/pgml.ML

2009-10-20 wenzelm [Tue, 20 Oct 2009 23:25:04 +0200] rev 33034
eliminated THENL -- use THEN RANGE;
eliminated TRY' -- use TRY with op o;
observe naming convention ctxt: Proof.context;
tuned whitespace;
src/HOL/Nominal/nominal_fresh_fun.ML

2009-10-20 wenzelm [Tue, 20 Oct 2009 22:46:24 +0200] rev 33033
tuned;
src/Pure/context.ML

2009-10-20 wenzelm [Tue, 20 Oct 2009 21:37:06 +0200] rev 33032
fixed SML/NJ toplevel pp;
tuned;
src/Pure/pure_setup.ML

2009-10-20 wenzelm [Tue, 20 Oct 2009 21:26:45 +0200] rev 33031
backpatching of structure Proof and ProofContext -- avoid odd aliases;
renamed transfer_proof to raw_transfer;
indicate firm naming conventions for theory, Proof.context, Context.generic;
src/Pure/Isar/proof.ML src/Pure/Isar/proof_context.ML src/Pure/context.ML src/Pure/meta_simplifier.ML

2009-10-20 wenzelm [Tue, 20 Oct 2009 21:22:37 +0200] rev 33030
tuned;
src/HOL/Decision_Procs/Approximation.thy src/HOL/Library/Sum_Of_Squares/positivstellensatz_tools.ML src/Pure/ProofGeneral/proof_general_pgip.ML

2009-10-20 wenzelm [Tue, 20 Oct 2009 20:54:31 +0200] rev 33029
uniform use of Integer.min/max;
src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML src/HOL/SMT/Tools/z3_proof_terms.ML src/HOL/Tools/Function/scnp_solve.ML src/HOL/Tools/Groebner_Basis/groebner.ML src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML src/HOL/Tools/prop_logic.ML src/HOL/Tools/quickcheck_generators.ML src/HOL/Tools/record.ML src/HOL/Tools/res_hol_clause.ML src/HOL/ex/predicate_compile.ML src/Provers/splitter.ML src/Pure/General/integer.ML src/Pure/Tools/find_theorems.ML src/Pure/meta_simplifier.ML src/Tools/Code/code_thingol.ML src/Tools/atomize_elim.ML

2009-10-20 wenzelm [Tue, 20 Oct 2009 20:03:23 +0200] rev 33028
modernized session SET_Protocol;
Admin/isatest/isatest-stats src/HOL/IsaMakefile src/HOL/README.html src/HOL/SET-Protocol/Cardholder_Registration.thy src/HOL/SET-Protocol/EventSET.thy src/HOL/SET-Protocol/Merchant_Registration.thy src/HOL/SET-Protocol/MessageSET.thy src/HOL/SET-Protocol/PublicSET.thy src/HOL/SET-Protocol/Purchase.thy src/HOL/SET-Protocol/ROOT.ML src/HOL/SET-Protocol/document/root.tex src/HOL/SET_Protocol/Cardholder_Registration.thy src/HOL/SET_Protocol/Event_SET.thy src/HOL/SET_Protocol/Merchant_Registration.thy src/HOL/SET_Protocol/Message_SET.thy src/HOL/SET_Protocol/Public_SET.thy src/HOL/SET_Protocol/Purchase.thy src/HOL/SET_Protocol/ROOT.ML src/HOL/SET_Protocol/document/root.tex