2012-03-16 huffman [Fri, 16 Mar 2012 15:51:53 +0100] rev 46962
make more word theorems respect int/bin distinction
src/HOL/Word/Word.thy

2012-03-16 wenzelm [Fri, 16 Mar 2012 18:20:12 +0100] rev 46961
outer syntax command definitions based on formal command_spec derived from theory header declarations;
NEWS src/HOL/Boogie/Tools/boogie_commands.ML src/HOL/HOLCF/Tools/Domain/domain.ML src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML src/HOL/HOLCF/Tools/cpodef.ML src/HOL/HOLCF/Tools/domaindef.ML src/HOL/HOLCF/Tools/fixrec.ML src/HOL/Import/import.ML src/HOL/Nominal/nominal_atoms.ML src/HOL/Nominal/nominal_datatype.ML src/HOL/Nominal/nominal_inductive.ML src/HOL/Nominal/nominal_inductive2.ML src/HOL/Nominal/nominal_primrec.ML src/HOL/Orderings.thy src/HOL/SPARK/Tools/spark_commands.ML src/HOL/Statespace/state_space.ML src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML src/HOL/Tools/Datatype/datatype.ML src/HOL/Tools/Datatype/primrec.ML src/HOL/Tools/Datatype/rep_datatype.ML src/HOL/Tools/Function/fun.ML src/HOL/Tools/Function/function.ML src/HOL/Tools/Function/partial_function.ML src/HOL/Tools/Nitpick/nitpick_isar.ML src/HOL/Tools/Predicate_Compile/code_prolog.ML src/HOL/Tools/Predicate_Compile/predicate_compile.ML src/HOL/Tools/Quickcheck/abstract_generators.ML src/HOL/Tools/Quickcheck/find_unused_assms.ML src/HOL/Tools/Quotient/quotient_def.ML src/HOL/Tools/Quotient/quotient_info.ML src/HOL/Tools/Quotient/quotient_type.ML src/HOL/Tools/SMT/smt_config.ML src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML src/HOL/Tools/choice_specification.ML src/HOL/Tools/enriched_type.ML src/HOL/Tools/inductive.ML src/HOL/Tools/inductive_set.ML src/HOL/Tools/recdef.ML src/HOL/Tools/record.ML src/HOL/Tools/refute.ML src/HOL/Tools/try0.ML src/HOL/Tools/typedef.ML src/Provers/classical.ML src/Pure/Isar/isar_syn.ML src/Pure/Isar/keyword.ML src/Pure/Isar/outer_syntax.ML src/Pure/ML/ml_antiquote.ML src/Pure/Proof/extraction.ML src/Pure/ProofGeneral/proof_general_emacs.ML src/Pure/ProofGeneral/proof_general_pgip.ML ...

2012-03-16 wenzelm [Fri, 16 Mar 2012 14:46:13 +0100] rev 46960
refute_params are given in *this* theory;
src/HOL/Refute.thy src/HOL/Tools/refute.ML

2012-03-16 wenzelm [Fri, 16 Mar 2012 14:42:11 +0100] rev 46959
defer actual parsing of command spans and thus allow new commands to be used in the same theory where defined;
NEWS src/Pure/Isar/toplevel.ML src/Pure/Thy/thy_load.ML

2012-03-16 wenzelm [Fri, 16 Mar 2012 13:05:30 +0100] rev 46958
define keywords early when processing the theory header, before running the body commands;
src/Pure/Isar/isar_syn.ML src/Pure/Isar/keyword.ML src/Pure/Isar/outer_syntax.ML src/Pure/PIDE/document.ML src/Pure/Thy/thy_header.ML src/Pure/Thy/thy_info.ML src/Pure/Thy/thy_load.ML src/Pure/Thy/thy_output.ML

2012-03-16 wenzelm [Fri, 16 Mar 2012 11:26:55 +0100] rev 46957
clarified Keyword.is_keyword: union of minor and major;
misc tuning and simplification;
src/HOL/Tools/Sledgehammer/sledgehammer_util.ML src/Pure/Isar/keyword.ML src/Pure/Isar/outer_syntax.ML src/Pure/ProofGeneral/proof_general_pgip.ML src/Pure/Thy/thy_output.ML

2012-03-15 wenzelm [Thu, 15 Mar 2012 23:06:22 +0100] rev 46956
Isabelle/jEdit supports user-defined Isar commands within the running session;
NEWS src/Tools/jEdit/README.html

2012-03-15 wenzelm [Thu, 15 Mar 2012 22:21:28 +0100] rev 46955
merged
src/ZF/upair.thy

2012-03-15 paulson [Thu, 15 Mar 2012 17:38:05 +0000] rev 46954
beautification and structured proofs
src/ZF/AC/HH.thy src/ZF/AC/WO2_AC16.thy src/ZF/Cardinal_AC.thy src/ZF/Nat_ZF.thy src/ZF/Ordinal.thy src/ZF/UNITY/AllocBase.thy

2012-03-15 paulson [Thu, 15 Mar 2012 16:35:02 +0000] rev 46953
replacing ":" by "\<in>"
src/ZF/AC.thy src/ZF/Bin.thy src/ZF/Cardinal.thy src/ZF/CardinalArith.thy src/ZF/Constructible/Formula.thy src/ZF/Constructible/Relative.thy src/ZF/Epsilon.thy src/ZF/EquivClass.thy src/ZF/Finite.thy src/ZF/Induct/Multiset.thy src/ZF/IntArith.thy src/ZF/Int_ZF.thy src/ZF/List_ZF.thy src/ZF/Main_ZF.thy src/ZF/Nat_ZF.thy src/ZF/OrdQuant.thy src/ZF/Order.thy src/ZF/OrderArith.thy src/ZF/OrderType.thy src/ZF/Ordinal.thy src/ZF/Perm.thy src/ZF/QPair.thy src/ZF/Sum.thy src/ZF/Trancl.thy src/ZF/UNITY/ClientImpl.thy src/ZF/UNITY/GenPrefix.thy src/ZF/UNITY/SubstAx.thy src/ZF/UNITY/Union.thy src/ZF/UNITY/WFair.thy src/ZF/WF.thy src/ZF/ex/Group.thy src/ZF/func.thy src/ZF/pair.thy src/ZF/upair.thy