| Mon, 10 Jan 2011 16:45:28 +0100 |
wenzelm |
added merge_options convenience;
|
file |
diff |
annotate
|
| Fri, 17 Dec 2010 17:08:56 +0100 |
wenzelm |
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
|
file |
diff |
annotate
|
| Mon, 31 May 2010 21:06:57 +0200 |
wenzelm |
modernized some structure names, keeping a few legacy aliases;
|
file |
diff |
annotate
|
| Mon, 03 May 2010 14:25:56 +0200 |
wenzelm |
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
|
file |
diff |
annotate
|
| Sun, 07 Mar 2010 12:47:02 +0100 |
wenzelm |
separate structure Typedecl;
|
file |
diff |
annotate
|
| Sun, 07 Mar 2010 12:19:47 +0100 |
wenzelm |
modernized structure Object_Logic;
|
file |
diff |
annotate
|
| Mon, 15 Feb 2010 17:17:51 +0100 |
wenzelm |
discontinued unnamed infix syntax;
|
file |
diff |
annotate
|
| Sun, 08 Nov 2009 18:43:42 +0100 |
wenzelm |
adapted Theory_Data;
|
file |
diff |
annotate
|
| Sat, 24 Oct 2009 18:55:47 +0200 |
wenzelm |
tuned message;
|
file |
diff |
annotate
|
| Sat, 07 Mar 2009 22:16:50 +0100 |
wenzelm |
more uniform handling of binding in targets and derived elements;
|
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
|
| Thu, 16 Oct 2008 22:44:29 +0200 |
wenzelm |
Drule.norm_hhf_eqs;
|
file |
diff |
annotate
|
| Mon, 07 Apr 2008 21:25:18 +0200 |
wenzelm |
renamed iterated forall_conv to params_conv;
|
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
|
| Wed, 28 Nov 2007 16:44:24 +0100 |
wenzelm |
added base_sort;
|
file |
diff |
annotate
|
| Sat, 13 Oct 2007 17:16:41 +0200 |
wenzelm |
replaced obsolete Theory.add_finals_i by Theory.add_deps;
|
file |
diff |
annotate
|
| Thu, 04 Oct 2007 20:29:24 +0200 |
wenzelm |
replaced literal 'a by Name.aT;
|
file |
diff |
annotate
|
| Thu, 04 Oct 2007 16:59:28 +0200 |
wenzelm |
Conv.forall_conv: proper context;
|
file |
diff |
annotate
|
| Sun, 29 Jul 2007 14:29:54 +0200 |
wenzelm |
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
|
file |
diff |
annotate
|
| Thu, 05 Jul 2007 20:01:39 +0200 |
wenzelm |
tuned interfaces: atomize, atomize_prems, atomize_prems_tac;
|
file |
diff |
annotate
|
| Thu, 05 Jul 2007 00:06:25 +0200 |
wenzelm |
avoid polymorphic equality;
|
file |
diff |
annotate
|
| Wed, 04 Jul 2007 16:49:34 +0200 |
wenzelm |
replaced HOLogic.Trueprop_conv by ObjectLogic.judgment_conv;
|
file |
diff |
annotate
|
| Tue, 03 Jul 2007 17:17:15 +0200 |
wenzelm |
CONVERSION tactical;
|
file |
diff |
annotate
|
| Thu, 10 May 2007 00:39:45 +0200 |
wenzelm |
moved conversions to structure Conv;
|
file |
diff |
annotate
|
| Mon, 07 May 2007 00:49:59 +0200 |
wenzelm |
simplified DataFun interfaces;
|
file |
diff |
annotate
|
| Thu, 26 Apr 2007 12:00:05 +0200 |
wenzelm |
renamed some old names Theory.xxx to Sign.xxx;
|
file |
diff |
annotate
|
| Thu, 07 Dec 2006 23:16:55 +0100 |
wenzelm |
reorganized structure Tactic vs. MetaSimplifier;
|
file |
diff |
annotate
|
| Thu, 07 Dec 2006 00:42:04 +0100 |
wenzelm |
reorganized structure Goal vs. Tactic;
|
file |
diff |
annotate
|