src/Tools/induct.ML
2011-06-08 wenzelm 2011-06-08 more robust exception pattern General.Subscript;
2011-04-27 wenzelm 2011-04-27 reorganized fixes as specialized (global) name space;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-04-08 wenzelm 2011-04-08 explicit structure Syntax_Trans; discontinued old-style constrainAbsC;
2010-12-17 wenzelm 2010-12-17 renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
2010-08-25 wenzelm 2010-08-25 renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
2010-06-24 wenzelm 2010-06-24 misc tuning;
2010-06-24 wenzelm 2010-06-24 tuned auxiliary structures;
2010-06-24 wenzelm 2010-06-24 Net.encode_type;
2010-05-17 wenzelm 2010-05-17 prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax; eliminated old-style structure aliases K = Keyword, P = Parse;
2010-04-30 wenzelm 2010-04-30 slightly more standard induct_simp_add/del attributes; provide explicit context for internal addsimps;
2010-03-07 wenzelm 2010-03-07 modernized structure Object_Logic;
2010-03-07 wenzelm 2010-03-07 modernized structure Local_Defs;
2010-02-27 wenzelm 2010-02-27 type/const name: explicitly allow abbreviations as well;
2010-02-25 wenzelm 2010-02-25 clarified ProofContext.read_type_name/Args.type_name wrt strict logical constructors;
2010-01-30 berghofe 2010-01-30 Added infrastructure for simplifying equality constraints in cases rules.
2010-01-10 berghofe 2010-01-10 Added infrastructure for simplifying equality constraints. Option (no_simp) restores old behaviour of induct method.
2009-11-25 haftmann 2009-11-25 normalized uncurry take/drop
2009-11-24 haftmann 2009-11-24 curried take/drop
2009-11-08 wenzelm 2009-11-08 adapted Generic_Data, Proof_Data; tuned;
2009-11-01 wenzelm 2009-11-01 adapted Item_Net; tuned;
2009-11-01 wenzelm 2009-11-01 modernized structure Rule_Cases;
2009-10-29 wenzelm 2009-10-29 separate "inner_rule" tag indicates parts of induction rules -- avoids unclear overlap with "internal" tag;
2009-10-02 wenzelm 2009-10-02 eliminated dead code;
2009-08-28 wenzelm 2009-08-28 modernized messages -- eliminated ctyp/cterm operations;
2009-07-25 wenzelm 2009-07-25 eliminated redundant Library.multiply;
2009-07-24 wenzelm 2009-07-24 renamed functor InductFun to Induct;
2009-07-21 wenzelm 2009-07-21 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
2009-07-17 wenzelm 2009-07-17 tuned/modernized Envir operations;
2009-03-26 wenzelm 2009-03-26 simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;
2009-03-17 wenzelm 2009-03-17 adapted to general Item_Net;
2009-03-15 wenzelm 2009-03-15 simplified attribute setup;
2009-03-13 wenzelm 2009-03-13 simplified method setup;
2009-03-13 wenzelm 2009-03-13 unified type Proof.method and pervasive METHOD combinators;
2009-03-03 wenzelm 2009-03-03 Thm.binding;
2009-01-21 haftmann 2009-01-21 binding is alias for Binding.T
2008-12-31 wenzelm 2008-12-31 qualified Term.rename_wrt_term;
2008-12-04 haftmann 2008-12-04 cleaned up binding module and related code
2008-09-26 wenzelm 2008-09-26 eliminated polymorphic equality;
2008-09-02 wenzelm 2008-09-02 explicit type Name.binding for higher-specification elements;
2008-08-14 wenzelm 2008-08-14 moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
2008-08-09 wenzelm 2008-08-09 unified Args.T with OuterLex.token, renamed some operations;
2008-06-26 wenzelm 2008-06-26 Args.context;
2008-06-23 wenzelm 2008-06-23 tuned get_inductT: *all* rules for missing instantiation; exported get_inductT;
2008-06-10 wenzelm 2008-06-10 added del attributes; tuned;
2008-05-18 wenzelm 2008-05-18 guess_instance: proper context;
2008-05-16 wenzelm 2008-05-16 removed obsolete option open; tuned comments;
2008-04-17 wenzelm 2008-04-17 adapted to ProofContext.revert_skolem: extra Name.clean required;
2008-04-12 wenzelm 2008-04-12 rep_cterm/rep_thm: no longer dereference theory_ref;
2008-04-07 wenzelm 2008-04-07 renamed iterated forall_conv to params_conv;
2008-03-15 wenzelm 2008-03-15 tuned messages;
2008-01-26 wenzelm 2008-01-26 avoid redundant escaping of Isabelle symbols;
2008-01-24 wenzelm 2008-01-24 replaced ContextPosition by Position.thread_data;
2007-10-19 wenzelm 2007-10-19 warn_open: context position;
2007-10-09 wenzelm 2007-10-09 generic Syntax.pretty/string_of operations;
2007-10-06 wenzelm 2007-10-06 simplified interfaces for outer syntax;
2007-10-05 wenzelm 2007-10-05 (co)induct: polymorhic taking'';
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;