src/Tools/induct.ML
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;