| Wed, 19 Jul 2000 12:33:19 +0200 | paulson | changed / to // for quotienting; general tidying | changeset | files |
| Wed, 19 Jul 2000 12:28:32 +0200 | paulson | renamed // to / (which is what we want anyway) to avoid clash with the new | changeset | files |
| Wed, 19 Jul 2000 10:59:59 +0200 | paulson | deleted redundant proof | changeset | files |
| Wed, 19 Jul 2000 10:55:50 +0200 | paulson | // change; also moved entry for AddIffs | changeset | files |
| Tue, 18 Jul 2000 21:44:42 +0200 | wenzelm | addsplits [split_if]; | changeset | files |
| Tue, 18 Jul 2000 21:09:18 +0200 | wenzelm | theorems foo.splits = foo.split foo.split_asm; | changeset | files |
| Tue, 18 Jul 2000 21:08:57 +0200 | wenzelm | removed obsolete expand_if = split_if; | changeset | files |
| Tue, 18 Jul 2000 21:08:40 +0200 | wenzelm | * HOL: removed obsolete expand_if = split_if; theorems if_splits = | changeset | files |