| Tue, 04 Nov 1997 16:17:04 +0100 |
wenzelm |
type object = exn (enhance readability);
|
file |
diff |
annotate
|
| Mon, 03 Nov 1997 11:56:53 +0100 |
wenzelm |
new implicit simpset mechanism based on Sign.sg anytype data;
|
file |
diff |
annotate
|
| Mon, 29 Sep 1997 11:45:52 +0200 |
paulson |
Default simpset tactics now dereference "simpset"
|
file |
diff |
annotate
|
| Fri, 25 Jul 1997 13:18:09 +0200 |
wenzelm |
added prems argument to simplification procedures;
|
file |
diff |
annotate
|
| Wed, 23 Jul 1997 11:03:54 +0200 |
wenzelm |
added simplification meta rules;
|
file |
diff |
annotate
|
| Tue, 22 Jul 1997 18:46:44 +0200 |
wenzelm |
added print_ss;
|
file |
diff |
annotate
|
| Tue, 22 Jul 1997 11:12:55 +0200 |
paulson |
Removal of the tactical STATE
|
file |
diff |
annotate
|
| Wed, 16 Jul 1997 11:34:42 +0200 |
wenzelm |
fixed merge of internal simprocs;
|
file |
diff |
annotate
|
| Mon, 17 Feb 1997 13:54:24 +0100 |
wenzelm |
mk_rews: automatically includes strip_shyps, zero_var_indexes;
|
file |
diff |
annotate
|
| Sat, 15 Feb 1997 16:14:35 +0100 |
oheimb |
added deleqcongs, richer rep_ss
|
file |
diff |
annotate
|
| Fri, 31 Jan 1997 15:54:00 +0100 |
oheimb |
added addloop (and also documentation of addsolver
|
file |
diff |
annotate
|
| Fri, 17 Jan 1997 18:19:57 +0100 |
wenzelm |
addsimps, addeqcongs: replaced @ by gen_union;
|
file |
diff |
annotate
|
| Thu, 16 Jan 1997 14:53:37 +0100 |
wenzelm |
added termless parameter;
|
file |
diff |
annotate
|
| Fri, 10 Jan 1997 10:27:57 +0100 |
wenzelm |
cleaned up (real changes next time);
|
file |
diff |
annotate
|
| Wed, 29 May 1996 12:03:32 +0200 |
nipkow |
Added addsolver
|
file |
diff |
annotate
|
| Tue, 23 Apr 1996 17:11:23 +0200 |
oheimb |
*** empty log message ***
|
file |
diff |
annotate
|
| Fri, 16 Feb 1996 18:00:47 +0100 |
paulson |
Elimination of fully-functorial style.
|
file |
diff |
annotate
|
| Wed, 04 Oct 1995 12:53:35 +0100 |
clasohm |
renamed SS to Simpset; fixed bug in merge_ss
|
file |
diff |
annotate
|
| Fri, 01 Sep 1995 13:32:13 +0200 |
clasohm |
added global simpset
|
file |
diff |
annotate
|
| Thu, 30 Mar 1995 13:48:30 +0200 |
lcp |
Precedence of infixes is now 4 (just above that of :=)
|
file |
diff |
annotate
|
| Tue, 21 Jun 1994 11:55:36 +0200 |
nipkow |
improved error msg
|
file |
diff |
annotate
|
| Tue, 31 May 1994 13:17:41 +0200 |
nipkow |
simpset is hidden in a functor now.
|
file |
diff |
annotate
|
| Wed, 05 Jan 1994 19:47:14 +0100 |
nipkow |
got rid of METAHYPS due to the change of the basic simplification routines
|
file |
diff |
annotate
|
| Thu, 25 Nov 1993 13:41:08 +0100 |
nipkow |
asm_full_simp_tac now fails if there are no subgoals
|
file |
diff |
annotate
|
| Fri, 29 Oct 1993 11:54:50 +0100 |
nipkow |
added infix delsimps
|
file |
diff |
annotate
|
| Fri, 01 Oct 1993 13:26:22 +0100 |
nipkow |
asm_full_simp_tac now fails when applied to a state w/o subgoals.
|
file |
diff |
annotate
|
| Thu, 16 Sep 1993 14:21:44 +0200 |
nipkow |
changed addcongs to addeqcongs in simplifier.ML
|
file |
diff |
annotate
|
| Thu, 16 Sep 1993 12:20:38 +0200 |
clasohm |
Initial revision
|
file |
diff |
annotate
|