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 ...

2014-03-21 wenzelm [Fri, 21 Mar 2014 15:12:03 +0100] rev 56244
more qualified names;
src/HOL/Tools/ATP/atp_problem_generate.ML src/Pure/Proof/proof_rewrite_rules.ML src/Pure/logic.ML src/Pure/pure_thy.ML

2014-03-21 wenzelm [Fri, 21 Mar 2014 12:34:50 +0100] rev 56243
more qualified names;
src/Doc/IsarImplementation/Logic.thy src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML src/HOL/Library/Countable.thy src/HOL/Library/refute.ML src/HOL/Mutabelle/mutabelle_extra.ML src/HOL/Tools/ATP/atp_problem_generate.ML src/HOL/Tools/Nitpick/nitpick_hol.ML src/HOL/Tools/Nitpick/nitpick_preproc.ML src/HOL/Typerep.thy src/Pure/Proof/proof_syntax.ML src/Pure/Syntax/syntax_phases.ML src/Pure/Syntax/syntax_trans.ML src/Pure/logic.ML src/Pure/primitive_defs.ML src/Pure/pure_thy.ML src/Pure/term.ML

2014-03-21 wenzelm [Fri, 21 Mar 2014 12:14:33 +0100] rev 56242
tuned;
src/HOL/Tools/Quickcheck/narrowing_generators.ML

2014-03-21 wenzelm [Fri, 21 Mar 2014 11:42:32 +0100] rev 56241
more qualified names;
src/HOL/Code_Evaluation.thy src/HOL/List.thy src/HOL/Mutabelle/mutabelle_extra.ML src/HOL/Tools/Ctr_Sugar/case_translation.ML src/HOL/Tools/Quickcheck/exhaustive_generators.ML src/Pure/Proof/proof_syntax.ML src/Pure/Syntax/syntax_phases.ML src/Pure/pure_thy.ML src/Pure/term.ML src/Tools/Code/code_thingol.ML

2014-03-21 wenzelm [Fri, 21 Mar 2014 11:06:39 +0100] rev 56240
tuned signature;
src/Doc/Codegen/Setup.thy src/HOL/Imperative_HOL/Overview.thy src/Pure/Isar/isar_syn.ML src/Pure/Proof/proof_syntax.ML src/Pure/pure_thy.ML src/Pure/sign.ML

2014-03-21 wenzelm [Fri, 21 Mar 2014 10:45:03 +0100] rev 56239
tuned signature;
src/Doc/Codegen/Setup.thy src/HOL/HOLCF/Tools/cont_consts.ML src/HOL/Imperative_HOL/Overview.thy src/HOL/Import/import_rule.ML src/HOL/Library/bnf_decl.ML src/HOL/Nominal/nominal_datatype.ML src/HOL/SPARK/Tools/spark_vcs.ML src/HOL/Tools/Datatype/datatype.ML src/HOL/Tools/Datatype/rep_datatype.ML src/HOL/Tools/Function/size.ML src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML src/Pure/Isar/isar_syn.ML src/Pure/Isar/object_logic.ML src/Pure/Proof/extraction.ML src/Pure/Proof/proof_syntax.ML src/Pure/pure_thy.ML src/Pure/sign.ML src/ZF/Tools/datatype_package.ML