| Thu, 23 Oct 1997 12:47:59 +0200 |
wenzelm |
Sign.stamp_names_of;
|
file |
diff |
annotate
|
| Fri, 17 Oct 1997 18:14:48 +0200 |
wenzelm |
adapted to qualified names;
|
file |
diff |
annotate
|
| Thu, 24 Jul 1997 11:13:12 +0200 |
nipkow |
Replaced clumsy rewriting by the new function simplify on thms.
|
file |
diff |
annotate
|
| Wed, 23 Jul 1997 10:34:18 +0200 |
wenzelm |
tmp fix to accomodate rep_ss changes;
|
file |
diff |
annotate
|
| Fri, 04 Jul 1997 12:32:31 +0200 |
paulson |
Now catches the error of calling tgoalw when there are no goals to prove,
|
file |
diff |
annotate
|
| Mon, 23 Jun 1997 11:33:59 +0200 |
paulson |
Removal of structure Context and its replacement by a theorem list of
|
file |
diff |
annotate
|
| Thu, 05 Jun 1997 13:27:28 +0200 |
paulson |
Numerous simplifications and removal of HOL-isms
|
file |
diff |
annotate
|
| Tue, 03 Jun 1997 11:08:08 +0200 |
paulson |
More de-HOLification: using Free, Const, etc. instead of mk_var, mk_const
|
file |
diff |
annotate
|
| Mon, 26 May 1997 12:28:30 +0200 |
paulson |
Now checks the name of the function being defined
|
file |
diff |
annotate
|
| Thu, 22 May 1997 15:13:16 +0200 |
paulson |
New headers and other minor changes
|
file |
diff |
annotate
|
| Wed, 21 May 1997 10:57:38 +0200 |
paulson |
Basis library input/output primitives; currying the induction rule;
|
file |
diff |
annotate
|
| Tue, 20 May 1997 11:49:57 +0200 |
paulson |
Removal of redundant code (unused or already present in Isabelle.
|
file |
diff |
annotate
|
| Fri, 16 May 1997 10:43:44 +0200 |
paulson |
Subst now moved to directory HOL
|
file |
diff |
annotate
|
| Thu, 15 May 1997 12:29:59 +0200 |
paulson |
TFL now integrated with HOL (more work needed)
|
file |
diff |
annotate
|
| Fri, 03 Jan 1997 10:45:31 +0100 |
paulson |
Conversion to Basis Library (using prs instead of output)
|
file |
diff |
annotate
|
| Fri, 18 Oct 1996 12:41:04 +0200 |
paulson |
Konrad Slind's TFL
|
file |
diff |
annotate
|