| Fri, 18 Apr 1997 11:54:54 +0200 | paulson | Renamed sign constructors to eliminate clash with the Plus infix of Sum.thy | changeset | files |
| Fri, 18 Apr 1997 11:53:55 +0200 | paulson | Now loads theory LList indirectly: via LFilter | changeset | files |
| Fri, 18 Apr 1997 11:53:16 +0200 | paulson | Now uses some "case" syntax (but could use more) | changeset | files |
| Fri, 18 Apr 1997 11:52:44 +0200 | paulson | New monotonicity theorems | changeset | files |
| Fri, 18 Apr 1997 11:52:19 +0200 | paulson | New theory: a corecursive filter functional | changeset | files |
| Fri, 18 Apr 1997 11:48:16 +0200 | paulson | Removed needless parentheses from translation | changeset | files |
| Fri, 18 Apr 1997 11:47:36 +0200 | paulson | ex/LFilter is a new theory (and dependency) | changeset | files |