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