src/Pure/Isar/rule_insts.ML
Wed, 29 May 2013 18:25:11 +0200 wenzelm tuned signature -- more explicit flags for low-level Thm.bicompose;
Tue, 14 Feb 2012 22:27:33 +0100 wenzelm clarified bires_inst_tac: retain internal exceptions;
Tue, 14 Feb 2012 21:59:10 +0100 wenzelm more conventional tactic setup -- avoid low-level Thm.dest_state and spurious warnings about it;
Tue, 14 Feb 2012 17:49:47 +0100 wenzelm eliminated unused subgoals_tac;
Mon, 21 Nov 2011 23:04:45 +0100 wenzelm simplified read_instantiate -- no longer need to assign values, since rule attributes are now static;
Mon, 21 Nov 2011 21:38:08 +0100 wenzelm tuned;
Wed, 17 Aug 2011 18:05:31 +0200 wenzelm modernized signature of Term.absfree/absdummy;
Mon, 08 Aug 2011 17:23:15 +0200 wenzelm misc tuning -- eliminated old-fashioned rep_thm;
Thu, 09 Jun 2011 23:12:02 +0200 wenzelm renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate;
Sat, 14 May 2011 16:27:47 +0200 wenzelm modernized structure Rule_Insts;
Sat, 16 Apr 2011 15:47:52 +0200 wenzelm modernized structure Proof_Context;
Sun, 12 Sep 2010 19:04:02 +0200 wenzelm eliminated aliases of Type.constraint;
Thu, 27 May 2010 17:41:27 +0200 wenzelm renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
Mon, 17 May 2010 15:11:25 +0200 wenzelm renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
Sat, 15 May 2010 23:16:32 +0200 wenzelm refer directly to structure Keyword and Parse;
Sun, 01 Nov 2009 15:24:45 +0100 wenzelm modernized structure Rule_Cases;
Thu, 29 Oct 2009 17:58:26 +0100 wenzelm standardized filter/filter_out;
Wed, 30 Sep 2009 22:20:58 +0200 wenzelm eliminated redundant bindings;
Thu, 09 Jul 2009 22:48:12 +0200 wenzelm renamed structure TermSubst to Term_Subst;
Mon, 06 Jul 2009 21:24:30 +0200 wenzelm structure Thm: less pervasive names;
Sat, 28 Mar 2009 17:53:33 +0100 wenzelm renamed ProofContext.add_fixes_i to ProofContext.add_fixes, eliminated obsolete external version;
Thu, 26 Mar 2009 14:14:02 +0100 wenzelm simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;
Mon, 16 Mar 2009 19:40:03 +0100 wenzelm method parser: pass proper context;
Mon, 16 Mar 2009 17:47:26 +0100 wenzelm export method parser;
Sun, 15 Mar 2009 15:59:44 +0100 wenzelm simplified attribute setup;
Fri, 13 Mar 2009 23:50:05 +0100 wenzelm simplified method setup;
Fri, 13 Mar 2009 19:58:26 +0100 wenzelm unified type Proof.method and pervasive METHOD combinators;
Wed, 21 Jan 2009 23:21:44 +0100 wenzelm removed Ids;
Thu, 04 Dec 2008 14:43:33 +0100 haftmann cleaned up binding module and related code
Tue, 02 Sep 2008 14:10:45 +0200 wenzelm explicit type Name.binding for higher-specification elements;
Fri, 15 Aug 2008 15:50:44 +0200 wenzelm Args.name_source(_position) for proper position information;
Sat, 09 Aug 2008 22:43:46 +0200 wenzelm unified Args.T with OuterLex.token, renamed some operations;
Sat, 28 Jun 2008 15:17:26 +0200 wenzelm tuned;
Thu, 19 Jun 2008 20:48:06 +0200 wenzelm private add_used (from drule.ML);
Mon, 16 Jun 2008 22:13:54 +0200 wenzelm added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML);
Mon, 16 Jun 2008 17:54:50 +0200 wenzelm added read_instantiate;
Sat, 14 Jun 2008 23:20:12 +0200 wenzelm export subgoal_tac, subgoals_tac, thin_tac;
Tue, 10 Jun 2008 16:43:23 +0200 wenzelm added (e)res_inst_tac;
Fri, 28 Mar 2008 20:02:04 +0100 wenzelm Context.>> : operate on Context.generic;
Thu, 27 Mar 2008 15:32:15 +0100 wenzelm eliminated delayed theory setup
Thu, 08 Nov 2007 20:08:11 +0100 wenzelm where/of: do not allow schematic variables here!
Wed, 07 Nov 2007 22:20:12 +0100 wenzelm Syntax.read_typ;
Wed, 07 Nov 2007 16:43:01 +0100 wenzelm attribute where/of: proper Syntax.parse/check;
Sun, 15 Apr 2007 14:31:49 +0200 wenzelm proper ProofContext.infer_types;
Sat, 14 Apr 2007 17:36:09 +0200 wenzelm cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
Mon, 18 Dec 2006 08:21:35 +0100 haftmann switched argument order in *.syntax lifters
Thu, 23 Nov 2006 20:33:41 +0100 wenzelm renamed Args.Name to Args.Text;
Fri, 15 Sep 2006 22:56:13 +0200 wenzelm renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
Tue, 12 Sep 2006 12:12:46 +0200 wenzelm moved term subst functions to TermSubst;
Wed, 06 Sep 2006 22:48:36 +0200 wenzelm read_instantiate: declare names of TVars as well (temporary workaround for no-freeze feature of type inference);
Sat, 05 Aug 2006 14:52:58 +0200 wenzelm reworked read_instantiate -- separate read_insts;
Thu, 03 Aug 2006 17:30:44 +0200 wenzelm Rule instantiations -- operations within a rule/subgoal context.
less more (0) tip