| Thu, 05 Feb 1998 11:19:51 +0100 |
wenzelm |
added THEN_ALL_NEW;
|
file |
diff |
annotate
|
| Fri, 21 Nov 1997 15:27:43 +0100 |
wenzelm |
changed Sequence interface (now Seq, in seq.ML);
|
file |
diff |
annotate
|
| Fri, 24 Oct 1997 17:13:21 +0200 |
wenzelm |
ProtoPure.thy;
|
file |
diff |
annotate
|
| Thu, 11 Sep 1997 16:16:03 +0200 |
wenzelm |
removed print_goals_ref (which was broken anyway);
|
file |
diff |
annotate
|
| Wed, 23 Jul 1997 11:48:59 +0200 |
paulson |
Removal of tactical STATE
|
file |
diff |
annotate
|
| Tue, 18 Mar 1997 15:15:01 +0100 |
paulson |
A more explicit prefix because gensym now generates easily predicatable
|
file |
diff |
annotate
|
| Fri, 21 Feb 1997 15:31:47 +0100 |
paulson |
Replaced "flat" by the Basis Library function List.concat
|
file |
diff |
annotate
|
| Sat, 15 Feb 1997 16:05:07 +0100 |
oheimb |
added THEN_MAYBE and THEN_MAYBE'
|
file |
diff |
annotate
|
| Tue, 04 Feb 1997 10:33:58 +0100 |
paulson |
Gradual switching to Basis Library functions nth, drop, etc.
|
file |
diff |
annotate
|
| Wed, 27 Nov 1996 10:54:16 +0100 |
paulson |
Converted I/O operatios for Basis Library compatibility
|
file |
diff |
annotate
|
| Mon, 04 Nov 1996 10:56:15 +0100 |
paulson |
Renamed SELECT_GOAL's new parameter from x to selct to avoid clashes
|
file |
diff |
annotate
|
| Mon, 23 Sep 1996 17:46:12 +0200 |
paulson |
Optimized version of SELECT_GOAL, up to 10% faster
|
file |
diff |
annotate
|
| Thu, 04 Apr 1996 12:58:47 +0200 |
paulson |
Fixed error in CHANGED (caused by variable renaming)
|
file |
diff |
annotate
|
| Fri, 15 Mar 1996 18:39:08 +0100 |
paulson |
Search tacticals moved to search.ML
|
file |
diff |
annotate
|
| Fri, 16 Feb 1996 12:57:32 +0100 |
paulson |
Elimination of fully-functorial style.
|
file |
diff |
annotate
|
| Mon, 29 Jan 1996 14:16:13 +0100 |
clasohm |
inserted tabs again
|
file |
diff |
annotate
|
| Mon, 29 Jan 1996 13:56:41 +0100 |
clasohm |
removed tabs
|
file |
diff |
annotate
|
| Fri, 03 Mar 1995 11:48:05 +0100 |
clasohm |
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
|
file |
diff |
annotate
|
| Tue, 22 Nov 1994 23:32:16 +0100 |
lcp |
Pure/tctical/protect_subgoal: simplified to use Sequence.hd
|
file |
diff |
annotate
|
| Mon, 14 Nov 1994 10:49:39 +0100 |
lcp |
Pure/tctical/select: now uses cprems_of instead of prems_of and cterm_of:
|
file |
diff |
annotate
|
| Fri, 11 Nov 1994 10:41:09 +0100 |
lcp |
Pure/tctical/REPEAT_DETERM_N,REPEAT_DETERM1,REPEAT_DETERM_FIRST,
|
file |
diff |
annotate
|
| Mon, 31 Oct 1994 18:03:14 +0100 |
lcp |
Pure/tctical/THEN_ELSE: new
|
file |
diff |
annotate
|
| Wed, 12 Oct 1994 09:48:32 +0100 |
lcp |
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
|
file |
diff |
annotate
|
| Tue, 18 Jan 1994 15:57:40 +0100 |
lcp |
Many other files modified as follows:
|
file |
diff |
annotate
|
| Thu, 21 Oct 1993 17:20:01 +0100 |
lcp |
Pure/drule/print_goals_ref: new, for Centaur interface
|
file |
diff |
annotate
|
| Wed, 06 Oct 1993 10:33:33 +0100 |
lcp |
tctical/dummy_quant_rl: specifies type prop to avoid the type variable
|
file |
diff |
annotate
|
| Thu, 16 Sep 1993 12:20:38 +0200 |
clasohm |
Initial revision
|
file |
diff |
annotate
|