| Thu, 29 Mar 2007 14:21:45 +0200 |
haftmann |
dropped legacy ML bindings
|
file |
diff |
annotate
|
| Wed, 06 Dec 2006 01:12:36 +0100 |
wenzelm |
removed legacy ML bindings;
|
file |
diff |
annotate
|
| Mon, 27 Nov 2006 13:42:33 +0100 |
haftmann |
removed HOL structure
|
file |
diff |
annotate
|
| Fri, 13 Oct 2006 18:29:31 +0200 |
berghofe |
Adapted to changes in FixedPoint theory.
|
file |
diff |
annotate
|
| Tue, 10 Oct 2006 10:34:43 +0200 |
haftmann |
added legacy tactic
|
file |
diff |
annotate
|
| Fri, 07 Oct 2005 20:41:10 +0200 |
nipkow |
changes due to new neq_simproc in simpdata.ML
|
file |
diff |
annotate
|
| Tue, 06 Sep 2005 19:10:43 +0200 |
wenzelm |
converted to Isar theory format;
|
file |
diff |
annotate
|
| Wed, 08 Dec 2004 10:28:05 +0100 |
paulson |
converted Lfp to new-style theory
|
file |
diff |
annotate
|
| Thu, 12 Oct 2000 13:01:19 +0200 |
nipkow |
induct -> lfp_induct
|
file |
diff |
annotate
|
| Fri, 07 Jan 2000 11:06:03 +0100 |
paulson |
tidied parentheses
|
file |
diff |
annotate
|
| Tue, 07 Sep 1999 10:40:58 +0200 |
wenzelm |
isatool expandshort;
|
file |
diff |
annotate
|
| Thu, 06 Aug 1998 15:48:13 +0200 |
paulson |
even more tidying of Goal commands
|
file |
diff |
annotate
|
| Fri, 31 Jul 1998 11:03:21 +0200 |
paulson |
Removal of obsolete "open" commands from heads of .ML files
|
file |
diff |
annotate
|
| Wed, 15 Jul 1998 14:19:02 +0200 |
paulson |
More tidying and removal of "\!\!... from Goal commands
|
file |
diff |
annotate
|
| Wed, 15 Jul 1998 10:15:13 +0200 |
paulson |
Removal of leading "\!\!..." from most Goal commands
|
file |
diff |
annotate
|
| Mon, 22 Jun 1998 17:26:46 +0200 |
wenzelm |
isatool fixgoal;
|
file |
diff |
annotate
|
| Wed, 03 Dec 1997 11:00:24 +0100 |
paulson |
updated for latest Blast_tac, which treats equality differently
|
file |
diff |
annotate
|
| Wed, 05 Nov 1997 13:23:46 +0100 |
paulson |
Ran expandshort, especially to introduce Safe_tac
|
file |
diff |
annotate
|
| Mon, 03 Nov 1997 12:13:18 +0100 |
wenzelm |
isatool fixclasimp;
|
file |
diff |
annotate
|
| Fri, 10 Oct 1997 19:02:28 +0200 |
wenzelm |
fixed dots;
|
file |
diff |
annotate
|
| Fri, 11 Apr 1997 15:21:36 +0200 |
paulson |
Yet more fast_tac->blast_tac, and other tidying
|
file |
diff |
annotate
|
| Fri, 21 Jun 1996 12:18:50 +0200 |
berghofe |
Classical tactics now use default claset.
|
file |
diff |
annotate
|
| Fri, 15 Mar 1996 18:41:04 +0100 |
paulson |
Sets a lower value of Unify.search_bound
|
file |
diff |
annotate
|
| Tue, 30 Jan 1996 15:24:36 +0100 |
clasohm |
expanded tabs
|
file |
diff |
annotate
|
| Wed, 04 Oct 1995 13:12:14 +0100 |
clasohm |
added local simpsets
|
file |
diff |
annotate
|
| Thu, 13 Apr 1995 15:13:27 +0200 |
lcp |
Simplified some proofs and made them work for new hyp_subst_tac.
|
file |
diff |
annotate
|
| Fri, 24 Mar 1995 12:30:35 +0100 |
clasohm |
changed syntax of tuples from <..., ...> to (..., ...)
|
file |
diff |
annotate
|
| Wed, 22 Mar 1995 12:42:34 +0100 |
clasohm |
converted ex with curried function application
|
file |
diff |
annotate
|