src/Tools/induct.ML
Sat, 11 Sep 2021 22:07:43 +0200 wenzelm more antiquotations;
Fri, 10 Sep 2021 14:59:19 +0200 wenzelm clarified signature: more scalable operations;
Tue, 13 Aug 2019 10:27:21 +0200 wenzelm clarified modules;
Fri, 04 Jan 2019 23:22:53 +0100 wenzelm isabelle update -u control_cartouches;
Thu, 03 Jan 2019 22:19:19 +0100 wenzelm isabelle update_inner_syntax_cartouches;
Sun, 18 Feb 2018 15:05:21 +0100 wenzelm tuned signature;
Wed, 06 Dec 2017 20:43:09 +0100 wenzelm prefer control symbol antiquotations;
Wed, 22 Jun 2016 10:40:53 +0200 wenzelm tuned signature;
Tue, 12 Apr 2016 14:38:57 +0200 wenzelm Type_Infer.object_logic controls improvement of type inference result;
Fri, 08 Apr 2016 20:15:20 +0200 wenzelm eliminated unused simproc identifier;
Wed, 16 Dec 2015 16:31:36 +0100 wenzelm rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
Mon, 14 Dec 2015 11:20:31 +0100 wenzelm tuned signature;
Sun, 13 Dec 2015 21:56:15 +0100 wenzelm more general types Proof.method / context_tactic;
Fri, 25 Sep 2015 20:37:59 +0200 wenzelm moved remaining display.ML to more_thm.ML;
Wed, 09 Sep 2015 20:57:21 +0200 wenzelm simplified simproc programming interfaces;
Sun, 30 Aug 2015 22:07:55 +0200 wenzelm trim context for persistent storage;
Sun, 26 Jul 2015 17:24:54 +0200 wenzelm updated to infer_instantiate;
Sun, 05 Jul 2015 15:02:30 +0200 wenzelm simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
Thu, 25 Jun 2015 16:14:00 +0200 wenzelm tuned signature;
Thu, 25 Jun 2015 15:56:33 +0200 wenzelm tuned;
Sat, 13 Jun 2015 17:14:05 +0200 wenzelm implicit rule for method "cases";
Sat, 30 May 2015 20:21:53 +0200 wenzelm tuned -- more direct Thm.renamed_prop;
Thu, 16 Apr 2015 15:22:44 +0200 wenzelm discontinued pointless warnings: commands are only defined inside a theory context;
Wed, 08 Apr 2015 20:14:18 +0200 wenzelm tuned;
Wed, 08 Apr 2015 19:58:52 +0200 wenzelm tuned signature;
Wed, 08 Apr 2015 19:39:08 +0200 wenzelm proper context for Object_Logic operations;
Mon, 06 Apr 2015 23:14:05 +0200 wenzelm local setup of induction tools, with restricted access to auxiliary consts;
Mon, 06 Apr 2015 17:06:48 +0200 wenzelm @{command_spec} is superseded by @{command_keyword};
Mon, 06 Apr 2015 12:37:21 +0200 wenzelm tuned;
Sun, 29 Mar 2015 20:40:49 +0200 wenzelm tuned;
Fri, 06 Mar 2015 15:58:56 +0100 wenzelm Thm.cterm_of and Thm.ctyp_of operate on local context;
Wed, 04 Mar 2015 22:05:01 +0100 wenzelm clarified signature;
Wed, 04 Mar 2015 19:53:18 +0100 wenzelm tuned signature -- prefer qualified names;
Tue, 10 Feb 2015 14:48:26 +0100 wenzelm proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
Wed, 26 Nov 2014 20:05:34 +0100 wenzelm renamed "pairself" to "apply2", in accordance to @{apply 2};
Wed, 26 Nov 2014 16:55:43 +0100 wenzelm added ML antiquotation @{apply n} or @{apply n(k)};
Sun, 09 Nov 2014 17:04:14 +0100 wenzelm proper context for match_tac etc.;
Sun, 09 Nov 2014 14:08:00 +0100 wenzelm proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
Sat, 08 Nov 2014 21:31:51 +0100 wenzelm optional proof context for unify operations, for the sake of proper local options;
Mon, 03 Nov 2014 14:50:27 +0100 wenzelm eliminated unused int_only flag (see also c12484a27367);
Thu, 30 Oct 2014 16:55:29 +0100 wenzelm eliminated aliases;
Wed, 29 Oct 2014 19:01:49 +0100 wenzelm modernized setup;
Tue, 19 Aug 2014 12:05:11 +0200 wenzelm simplified type Proof.method;
Mon, 31 Mar 2014 12:35:39 +0200 wenzelm some shortcuts for chunks, which sometimes avoid bulky string output;
Fri, 21 Mar 2014 20:33:56 +0100 wenzelm more qualified names;
Thu, 20 Mar 2014 21:07:57 +0100 wenzelm enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES -- clean tactical failure if out-of-range;
Thu, 06 Mar 2014 13:44:01 +0100 wenzelm more uniform check_const/read_const;
Thu, 06 Mar 2014 12:10:19 +0100 wenzelm tuned signature -- more uniform check_type_name/read_type_name;
Sat, 14 Dec 2013 17:28:05 +0100 wenzelm proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
Fri, 23 Aug 2013 17:01:12 +0200 wenzelm tuned signature;
Sat, 27 Jul 2013 16:35:51 +0200 wenzelm standardized aliases;
Wed, 17 Jul 2013 13:45:55 +0200 wenzelm take context from static theory, not dynamic theory certificate;
Thu, 18 Apr 2013 17:07:01 +0200 wenzelm simplifier uses proper Proof.context instead of historic type simpset;
Tue, 09 Apr 2013 15:29:25 +0200 wenzelm discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
Sat, 30 Mar 2013 13:40:19 +0100 wenzelm more item markup;
Fri, 29 Mar 2013 22:14:27 +0100 wenzelm Pretty.item markup for improved readability of lists of items;
Tue, 09 Oct 2012 20:05:17 +0200 wenzelm clarified Local_Defs.add_def(s): refrain from hard-wiring Thm.def_binding_optional;
Sat, 29 Sep 2012 18:23:46 +0200 wenzelm more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;
Wed, 21 Mar 2012 11:00:34 +0100 wenzelm prefer explicitly qualified exception List.Empty;
Fri, 16 Mar 2012 18:20:12 +0100 wenzelm outer syntax command definitions based on formal command_spec derived from theory header declarations;
less more (0) -100 -60 tip