| Mon, 26 May 1997 12:36:56 +0200 | paulson | Two results suggested by Florian Kammueller | changeset | files |
| Mon, 26 May 1997 12:36:16 +0200 | paulson | Tidying and a couple of useful lemmas | changeset | files |
| Mon, 26 May 1997 12:34:54 +0200 | paulson | Added recdef | changeset | files |
| Mon, 26 May 1997 12:34:05 +0200 | paulson | Primrec: New example ported from ZF | changeset | files |
| Mon, 26 May 1997 12:33:38 +0200 | paulson | Renamed lessD to Suc_leI | changeset | files |
| Mon, 26 May 1997 12:33:03 +0200 | paulson | New example ported from ZF | changeset | files |
| Mon, 26 May 1997 12:32:35 +0200 | paulson | Simplified proofs using expand_option_case | changeset | files |
| Mon, 26 May 1997 12:29:55 +0200 | paulson | Now checks the name of the function being defined; | changeset | files |
| Mon, 26 May 1997 12:29:10 +0200 | paulson | More de-HOL-ification | changeset | files |
| Mon, 26 May 1997 12:28:30 +0200 | paulson | Now checks the name of the function being defined | changeset | files |
| Mon, 26 May 1997 12:27:58 +0200 | paulson | Deleted unused functions | changeset | files |
| Mon, 26 May 1997 12:26:35 +0200 | paulson | Now a Perl script. No longer requires commands to be at the beginnings of | changeset | files |
| Mon, 26 May 1997 12:25:15 +0200 | paulson | Slight simplifications | changeset | files |
| Sun, 25 May 1997 18:45:25 +0200 | slotosch | Eliminated ccc1. Moved ID,oo into Cfun. | changeset | files |
| Sun, 25 May 1997 16:59:40 +0200 | slotosch | Moved the classes flat chfin from Fix to Pcpo. | changeset | files |
| Sun, 25 May 1997 16:57:19 +0200 | slotosch | *** empty log message *** | changeset | files |
| Sun, 25 May 1997 16:17:09 +0200 | slotosch | Eliminated the prediates flat,chfin | changeset | files |
| Sun, 25 May 1997 11:07:52 +0200 | slotosch | eliminated the constant less by the introduction of the axclass sq_ord | changeset | files |
| Fri, 23 May 1997 18:55:28 +0200 | wenzelm | tuned; | changeset | files |
| Fri, 23 May 1997 18:20:20 +0200 | nipkow | arbitrary | changeset | files |
| Fri, 23 May 1997 18:17:53 +0200 | nipkow | Added `arbitrary' | changeset | files |
| Fri, 23 May 1997 14:52:45 +0200 | wenzelm | fixed; | changeset | files |
| Fri, 23 May 1997 14:49:39 +0200 | oheimb | new syntactic priority of lambda abstraction | changeset | files |
| Fri, 23 May 1997 14:48:10 +0200 | oheimb | adapted entry for addss, addSss | changeset | files |
| Fri, 23 May 1997 14:17:40 +0200 | nipkow | news. | changeset | files |
| Fri, 23 May 1997 14:13:51 +0200 | nipkow | Documented `size' function for datatypes. | changeset | files |
| Fri, 23 May 1997 13:39:22 +0200 | mueller | fixed a bug | changeset | files |
| Fri, 23 May 1997 13:31:59 +0200 | wenzelm | removed TFL from test; | changeset | files |