Tue, 05 Oct 1999 15:29:46 +0200 | berghofe | Added attribute rulify_prems (useful for modifying premises of introduction | file | diff | annotate |
Mon, 04 Oct 1999 21:46:49 +0200 | wenzelm | Tools/typedef_package.ML; | file | diff | annotate |
Fri, 13 Nov 1998 13:27:03 +0100 | paulson | no longer loads Fun so that the Fun proofs can use equalities.thy | file | diff | annotate |
Mon, 05 Feb 1996 21:27:16 +0100 | clasohm | expanded tabs; renamed subtype to typedef; | file | diff | annotate |
Fri, 03 Mar 1995 12:02:25 +0100 | clasohm | new version of HOL with curried function application | file | diff | annotate |