Tue, 25 Jul 2000 00:13:11 +0200 |
wenzelm |
added clarsimp method;
|
file |
diff |
annotate
|
Fri, 21 Jul 2000 17:46:43 +0200 |
oheimb |
strengthened force_tac by using new first_best_tac
|
file |
diff |
annotate
|
Fri, 31 Mar 2000 21:58:34 +0200 |
wenzelm |
added change_global/local_css;
|
file |
diff |
annotate
|
Wed, 15 Mar 2000 18:40:03 +0100 |
wenzelm |
include Splitter.split_modifiers;
|
file |
diff |
annotate
|
Fri, 28 Jan 2000 21:57:15 +0100 |
wenzelm |
HEADGOAL;
|
file |
diff |
annotate
|
Fri, 28 Jan 2000 12:12:06 +0100 |
wenzelm |
replaced FIRSTGOAL by FINDGOAL (backtracking!);
|
file |
diff |
annotate
|
Wed, 27 Oct 1999 19:29:47 +0200 |
oheimb |
clarsimp_tac now copes with the (unwanted) case that the simplifier splits
|
file |
diff |
annotate
|
Tue, 21 Sep 1999 17:26:50 +0200 |
wenzelm |
setup for refined facts handling;
|
file |
diff |
annotate
|
Thu, 02 Sep 1999 15:21:36 +0200 |
wenzelm |
renamed improper method 'clarsimp' to 'clarsimp_tac';
|
file |
diff |
annotate
|
Wed, 01 Sep 1999 21:22:56 +0200 |
wenzelm |
Method.insert_tac;
|
file |
diff |
annotate
|
Mon, 30 Aug 1999 17:26:43 +0200 |
wenzelm |
auto: CHANGED;
|
file |
diff |
annotate
|
Wed, 18 Aug 1999 20:47:31 +0200 |
wenzelm |
Method.modifier;
|
file |
diff |
annotate
|
Mon, 02 Aug 1999 17:58:46 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Fri, 30 Jul 1999 13:43:26 +0200 |
wenzelm |
eliminated METHOD0 in favour of same_tac;
|
file |
diff |
annotate
|
Sun, 29 Nov 1998 13:13:57 +0100 |
wenzelm |
method brute_force = ALLGOALS force_tac;
|
file |
diff |
annotate
|
Wed, 18 Nov 1998 11:01:48 +0100 |
wenzelm |
method setup;
|
file |
diff |
annotate
|
Fri, 23 Oct 1998 20:35:56 +0200 |
oheimb |
corrected auto_tac (applications of unsafe wrappers)
|
file |
diff |
annotate
|
Fri, 25 Sep 1998 14:06:00 +0200 |
paulson |
deleted illegal "op"
|
file |
diff |
annotate
|
Thu, 24 Sep 1998 17:17:56 +0200 |
oheimb |
removed addcongs2 and delcongs2
|
file |
diff |
annotate
|
Mon, 21 Sep 1998 23:17:28 +0200 |
oheimb |
improved addbefore and addSbefore
|
file |
diff |
annotate
|
Fri, 11 Sep 1998 17:20:58 +0200 |
oheimb |
added clarsimp_tac and Clarsimp_tac
|
file |
diff |
annotate
|
Thu, 30 Jul 1998 19:02:52 +0200 |
wenzelm |
functorized Clasimp module;
|
file |
diff |
annotate
|
Sat, 02 May 1998 16:46:17 +0200 |
wenzelm |
added CLASIMPSET(') tacticals;
|
file |
diff |
annotate
|
Fri, 01 May 1998 22:30:42 +0200 |
oheimb |
Auto_tac: now uses enhanced version of asm_full_simp_tac,
|
file |
diff |
annotate
|
Tue, 10 Mar 1998 18:26:27 +0100 |
oheimb |
renamed smart_tac to force_tac, slight improvement of force_tac
|
file |
diff |
annotate
|
Thu, 26 Feb 1998 15:45:33 +0100 |
oheimb |
added smart_tac
|
file |
diff |
annotate
|
Wed, 25 Feb 1998 20:25:27 +0100 |
oheimb |
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
|
file |
diff |
annotate
|