| 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
|
| Mon, 09 Oct 2006 02:20:05 +0200 |
wenzelm |
attribute: Context.mapping;
|
file |
diff |
annotate
|
| Tue, 14 Mar 2006 16:29:38 +0100 |
wenzelm |
added is_elim (from Provers/classical.ML);
|
file |
diff |
annotate
|
| Mon, 06 Feb 2006 20:59:06 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 29 Jan 2006 19:23:49 +0100 |
wenzelm |
moved treatment of object-logic equalities to local_defs.ML;
|
file |
diff |
annotate
|
| Sat, 28 Jan 2006 17:28:59 +0100 |
wenzelm |
removed unatomize;
|
file |
diff |
annotate
|
| Fri, 27 Jan 2006 19:03:13 +0100 |
wenzelm |
renamed reverse_atomize to unatomize;
|
file |
diff |
annotate
|
| Wed, 25 Jan 2006 00:21:41 +0100 |
wenzelm |
tuned atomize_cterm;
|
file |
diff |
annotate
|
| Sat, 21 Jan 2006 23:02:14 +0100 |
wenzelm |
simplified type attribute;
|
file |
diff |
annotate
|
| Thu, 19 Jan 2006 21:22:08 +0100 |
wenzelm |
setup: theory -> theory;
|
file |
diff |
annotate
|
| Wed, 04 Jan 2006 00:52:45 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 25 Nov 2005 18:58:41 +0100 |
wenzelm |
forall_conv ~1;
|
file |
diff |
annotate
|