2008-06-25 wenzelm 2008-06-25 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
2008-06-25 berghofe 2008-06-25 - Equivariance simpset used in proofs of strong induction and inversion rules now contains perm_simproc_app and perm_simproc_fun as well - first_order_matchs now eta-contracts terms before matching - Rewrote code for proving strong inversion rule to avoid failure when one of the arguments of the inductive predicate has an atom type
2008-06-16 wenzelm 2008-06-16 allE_Nil: only one copy, proven in regular theory source;
2008-06-11 wenzelm 2008-06-11 Drule.read_instantiate;
2008-05-18 wenzelm 2008-05-18 moved global pretty/string_of functions from Sign to Syntax;
2008-04-17 wenzelm 2008-04-17 prove_global: pass context;
2008-04-07 wenzelm 2008-04-07 renamed iterated forall_conv to params_conv;
2008-03-20 berghofe 2008-03-20 Equivariance prover now uses permutation simprocs as well.
2008-03-20 haftmann 2008-03-20 more antiquotations
2008-03-20 wenzelm 2008-03-20 simplified get_thm(s): back to plain name argument;
2008-03-19 wenzelm 2008-03-19 auxiliary dynamic_thm(s) for fact lookup;
2008-01-03 berghofe 2008-01-03 Implemented proof of strong case analysis rule.
2007-10-06 wenzelm 2007-10-06 simplified interfaces for outer syntax;
2007-10-05 wenzelm 2007-10-05 tuned Induct interface: prefer pred'' over set'';
2007-10-04 wenzelm 2007-10-04 Conv.forall_conv: proper context;
2007-10-04 wenzelm 2007-10-04 moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
2007-09-28 berghofe 2007-09-28 prove_strong_ind now uses InductivePackage.rulify.
2007-09-25 wenzelm 2007-09-25 proper Sign operations instead of Theory aliases;
2007-09-13 urbanc 2007-09-13 some cleaning up to do with contexts
2007-09-13 berghofe 2007-09-13 Generalized equivariance and nominal_inductive commands to inductive definitions involving arbitrary monotone operators.
2007-07-03 wenzelm 2007-07-03 Conjunction.mk_conjunction_balanced;
2007-05-10 wenzelm 2007-05-10 Thm.first_order_match;
2007-04-25 berghofe 2007-04-25 eqvt_tac now instantiates introduction rules before applying them.
2007-04-20 berghofe 2007-04-20 Modified eqvt_tac to avoid failure due to introduction rules whose premises contain variables that do not occur in the conclusion.
2007-04-19 berghofe 2007-04-19 nominal_inductive no longer proves equivariance.
2007-03-28 berghofe 2007-03-28 - Improved error messages in equivariance proof - Renamed <predicate>_eqvt to <predicate>.eqvt
2007-03-27 berghofe 2007-03-27 Implemented proof of strong induction rule.
2007-02-13 berghofe 2007-02-13 First steps towards strengthening of induction rules for inductively defined predicates involving nominal datatypes.