| Wed, 21 Jan 2009 23:21:44 +0100 |
wenzelm |
removed Ids;
|
file |
diff |
annotate
|
| Fri, 05 Dec 2008 08:04:53 +0100 |
haftmann |
dropped NameSpace.declare_base
|
file |
diff |
annotate
|
| Thu, 04 Dec 2008 14:43:33 +0100 |
haftmann |
cleaned up binding module and related code
|
file |
diff |
annotate
|
| Thu, 20 Nov 2008 19:06:02 +0100 |
haftmann |
dropped legacy naming code
|
file |
diff |
annotate
|
| Fri, 14 Nov 2008 08:50:10 +0100 |
haftmann |
namify and name_decl combinators
|
file |
diff |
annotate
|
| Thu, 13 Nov 2008 14:19:09 +0100 |
haftmann |
consider prefixes for name bindings of simprocs (a first approximation)
|
file |
diff |
annotate
|
| Tue, 02 Sep 2008 14:10:19 +0200 |
wenzelm |
name/var morphism operates on Name.binding;
|
file |
diff |
annotate
|
| Tue, 24 Jun 2008 19:43:14 +0200 |
wenzelm |
ML_Antiquote.value;
|
file |
diff |
annotate
|
| Thu, 29 May 2008 23:46:43 +0200 |
wenzelm |
proper context for attribute simplified;
|
file |
diff |
annotate
|
| Tue, 15 Apr 2008 16:12:05 +0200 |
wenzelm |
Thm.forall_elim_var(s);
|
file |
diff |
annotate
|
| Sat, 29 Mar 2008 22:55:57 +0100 |
wenzelm |
purely functional setup of claset/simpset/clasimpset;
|
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, 27 Mar 2008 14:41:10 +0100 |
wenzelm |
renamed ML_Context.the_context to ML_Context.the_global_context;
|
file |
diff |
annotate
|
| Sat, 01 Sep 2007 15:47:01 +0200 |
wenzelm |
replaced ProofContext.read_term/prop by general Syntax.read_term/prop;
|
file |
diff |
annotate
|
| Thu, 02 Aug 2007 12:06:27 +0200 |
wenzelm |
turned simp_depth_limit into configuration option;
|
file |
diff |
annotate
|
| Sat, 28 Jul 2007 20:40:30 +0200 |
wenzelm |
added attribute "simproc";
|
file |
diff |
annotate
|
| Sun, 08 Jul 2007 19:51:58 +0200 |
wenzelm |
replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
|
file |
diff |
annotate
|
| Thu, 05 Jul 2007 20:01:35 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 03 Jul 2007 17:17:11 +0200 |
wenzelm |
moved (asm_)rewrite_goal_tac from goal.ML to meta_simplifier.ML (no longer depends on SELECT_GOAL);
|
file |
diff |
annotate
|
| Thu, 24 May 2007 08:37:37 +0200 |
haftmann |
tuned Pure/General/name_space.ML
|
file |
diff |
annotate
|
| Mon, 07 May 2007 00:49:59 +0200 |
wenzelm |
simplified DataFun interfaces;
|
file |
diff |
annotate
|
| Mon, 23 Apr 2007 20:44:09 +0200 |
wenzelm |
def_simproc(_i): proper ProofContext.read/cert_terms;
|
file |
diff |
annotate
|
| Mon, 16 Apr 2007 16:11:03 +0200 |
haftmann |
canonical merge operations
|
file |
diff |
annotate
|
| Sun, 15 Apr 2007 23:25:50 +0200 |
wenzelm |
removed obsolete TypeInfer.logicT -- use dummyT;
|
file |
diff |
annotate
|
| Wed, 28 Feb 2007 22:05:44 +0100 |
wenzelm |
exported get_ss, map_ss;
|
file |
diff |
annotate
|
| Sun, 04 Feb 2007 22:02:16 +0100 |
wenzelm |
def_simproc(_i): tuned interface;
|
file |
diff |
annotate
|
| Mon, 29 Jan 2007 19:58:14 +0100 |
wenzelm |
added get_simproc, @{simproc};
|
file |
diff |
annotate
|
| Sun, 28 Jan 2007 23:29:15 +0100 |
wenzelm |
added def_simproc(_i) -- define named simprocs;
|
file |
diff |
annotate
|
| Sat, 20 Jan 2007 14:09:17 +0100 |
wenzelm |
added @{simpset};
|
file |
diff |
annotate
|