| Tue, 26 Sep 2006 13:34:35 +0200 | haftmann | handling of \<^const> syntax for case; explicit case names for induction rules for rep_datatype | changeset | files |
| Tue, 26 Sep 2006 13:34:17 +0200 | haftmann | tuned syntax for <= < | changeset | files |
| Tue, 26 Sep 2006 13:34:16 +0200 | haftmann | renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes | changeset | files |
| Tue, 26 Sep 2006 13:34:15 +0200 | haftmann | renamed 0 and 1 to HOL.zero and HOL.one respectivly | changeset | files |
| Tue, 26 Sep 2006 11:11:57 +0200 | paulson | fixed the definition of "depth" | changeset | files |
| Tue, 26 Sep 2006 11:09:33 +0200 | paulson | Abstraction now handles equations where the RHS is a lambda-expression; also, strings of lambdas | changeset | files |