2014-03-22 wenzelm [Sat, 22 Mar 2014 18:19:57 +0100] rev 56254
more antiquotations;
src/HOL/Tools/ATP/atp_problem_generate.ML src/HOL/Tools/ATP/atp_proof_reconstruct.ML src/HOL/Tools/BNF/bnf_comp.ML src/HOL/Tools/BNF/bnf_fp_def_sugar.ML src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML src/HOL/Tools/Datatype/datatype.ML src/HOL/Tools/Datatype/datatype_prop.ML src/HOL/Tools/Datatype/datatype_realizer.ML src/HOL/Tools/Datatype/rep_datatype.ML src/HOL/Tools/Function/fun.ML src/HOL/Tools/Function/function.ML src/HOL/Tools/Function/function_common.ML src/HOL/Tools/Nitpick/nitpick_model.ML src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML src/HOL/Tools/TFL/usyntax.ML src/HOL/Tools/choice_specification.ML src/HOL/Tools/hologic.ML src/HOL/Tools/inductive_realizer.ML src/HOL/Tools/record.ML src/HOL/Tools/transfer.ML

2014-03-22 wenzelm [Sat, 22 Mar 2014 18:16:54 +0100] rev 56253
more antiquotations;
src/HOL/Nominal/nominal_atoms.ML src/HOL/Nominal/nominal_datatype.ML src/HOL/Nominal/nominal_fresh_fun.ML src/HOL/Nominal/nominal_inductive.ML src/HOL/Nominal/nominal_inductive2.ML src/HOL/Nominal/nominal_permeq.ML

2014-03-22 wenzelm [Sat, 22 Mar 2014 18:15:09 +0100] rev 56252
more antiquotations;
src/HOL/Library/bnf_decl.ML src/HOL/Library/refute.ML src/HOL/Library/simps_case_conv.ML src/HOL/TPTP/TPTP_Proof_Reconstruction.thy

2014-03-22 wenzelm [Sat, 22 Mar 2014 18:12:08 +0100] rev 56251
tuned message;
src/Pure/ML/ml_antiquotations.ML

2014-03-22 wenzelm [Sat, 22 Mar 2014 16:50:52 +0100] rev 56250
more antiquotations;
src/CTT/CTT.thy src/ZF/OrdQuant.thy

2014-03-22 wenzelm [Sat, 22 Mar 2014 15:58:27 +0100] rev 56249
avoid hard-wired theory names;
src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML src/HOL/HOLCF/Tools/cpodef.ML src/HOL/HOLCF/Tools/domaindef.ML src/HOL/Tools/Datatype/datatype.ML src/HOL/Tools/inductive.ML src/HOL/Tools/recdef.ML src/HOL/Tools/record.ML src/ZF/Tools/datatype_package.ML src/ZF/Tools/inductive_package.ML

2014-03-22 haftmann [Sat, 22 Mar 2014 08:37:43 +0100] rev 56248
generalized and strengthened cong rules on compound operators, similar to 1ed737a98198
NEWS src/HOL/Complete_Lattices.thy src/HOL/Fun_Def.thy src/HOL/Hoare_Parallel/RG_Examples.thy src/HOL/Library/Extended_Real.thy src/HOL/Library/Old_Recdef.thy src/HOL/Tools/BNF/bnf_gfp_tactics.ML src/HOL/Tools/BNF/bnf_lfp_tactics.ML src/HOL/UNITY/Follows.thy src/HOL/UNITY/Transformers.thy src/HOL/UNITY/Union.thy

2014-03-21 wenzelm [Fri, 21 Mar 2014 22:54:16 +0100] rev 56247
added splash screen for jvm boot, which is important for initial encounter to avoid multiple copies running against each other;
Admin/Linux/Isabelle.run

2014-03-21 wenzelm [Fri, 21 Mar 2014 20:39:54 +0100] rev 56246
merged

2014-03-21 wenzelm [Fri, 21 Mar 2014 20:33:56 +0100] rev 56245
more qualified names;
NEWS src/CCL/Wfd.thy src/Doc/ProgProve/LaTeXsugar.thy src/FOL/simpdata.ML src/FOLP/hypsubst.ML src/FOLP/simp.ML src/HOL/Decision_Procs/cooper_tac.ML src/HOL/Decision_Procs/ferrack_tac.ML src/HOL/Decision_Procs/ferrante_rackoff.ML src/HOL/Decision_Procs/langford.ML src/HOL/Decision_Procs/mir_tac.ML src/HOL/Library/LaTeXsugar.thy src/HOL/Library/OptionalSugar.thy src/HOL/Library/refute.ML src/HOL/Matrix_LP/Compute_Oracle/compute.ML src/HOL/Mutabelle/mutabelle_extra.ML src/HOL/Nitpick_Examples/Core_Nits.thy src/HOL/Nitpick_Examples/Refute_Nits.thy src/HOL/Nominal/nominal_primrec.ML src/HOL/Nominal/nominal_thmdecls.ML src/HOL/Product_Type.thy src/HOL/Prolog/prolog.ML src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML src/HOL/TPTP/TPTP_Proof_Reconstruction.thy src/HOL/Tools/ATP/atp_problem_generate.ML src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML src/HOL/Tools/Datatype/primrec.ML src/HOL/Tools/Datatype/rep_datatype.ML src/HOL/Tools/Function/function_common.ML src/HOL/Tools/Function/function_lib.ML src/HOL/Tools/Lifting/lifting_def.ML src/HOL/Tools/Meson/meson.ML src/HOL/Tools/Meson/meson_clausify.ML src/HOL/Tools/Nitpick/nitpick.ML src/HOL/Tools/Nitpick/nitpick_hol.ML src/HOL/Tools/Nitpick/nitpick_mono.ML src/HOL/Tools/Nitpick/nitpick_nut.ML src/HOL/Tools/Nitpick/nitpick_preproc.ML src/HOL/Tools/Predicate_Compile/code_prolog.ML src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML src/HOL/Tools/Qelim/cooper.ML src/HOL/Tools/SMT/smt_normalize.ML src/HOL/Tools/SMT/smt_utils.ML src/HOL/Tools/SMT/z3_proof_reconstruction.ML src/HOL/Tools/SMT/z3_proof_tools.ML src/HOL/Tools/SMT2/smt2_normalize.ML src/HOL/Tools/SMT2/smt2_util.ML src/HOL/Tools/SMT2/z3_new_proof.ML ...