| Wed, 27 May 1998 12:23:45 +0200 | paulson | mk_all_imp: no longer creates goals that have beta-redexes | file | diff | annotate |
| Fri, 10 Apr 1998 13:42:22 +0200 | paulson | Fixed bug in inductive sections to allow disjunctive premises; | file | diff | annotate |
| Fri, 17 May 1996 12:23:44 +0200 | nipkow | Moved split_rule et al from ind_syntax.ML to Prod.ML. | file | diff | annotate |
| Tue, 07 May 1996 18:15:51 +0200 | paulson | Unfolding of arbitrarily nested tuples in induction rules | file | diff | annotate |
| Tue, 30 Jan 1996 15:24:36 +0100 | clasohm | expanded tabs | file | diff | annotate |
| Sat, 06 Jan 1996 14:04:12 +0100 | nipkow | removed reference to Nat thms in elim_rls. | file | diff | annotate |
| Tue, 02 Jan 1996 10:46:50 +0100 | paulson | Improving space efficiency of inductive/datatype definitions. | file | diff | annotate |
| Fri, 03 Mar 1995 12:02:25 +0100 | clasohm | new version of HOL with curried function application | file | diff | annotate |