| Wed, 01 Mar 1995 13:26:50 +0100 | lcp | Proved inj_onto_iff | file | diff | annotate |
| Mon, 21 Nov 1994 17:50:34 +0100 | clasohm | replaced 'val ... = result()' by 'qed "..."' | file | diff | annotate |
| Tue, 30 Aug 1994 10:04:49 +0200 | nipkow | New version of datatype.ML with primrec (Norbert). | file | diff | annotate |
| Thu, 25 Aug 1994 11:01:45 +0200 | lcp | INSTALLATION OF INDUCTIVE DEFINITIONS | file | diff | annotate |
| Fri, 19 Aug 1994 11:02:45 +0200 | lcp | HOL/fun.ML: renamed Fun.ML to avoid problems with MLs "fun" keyword | file | diff | annotate |