| Thu, 13 Jul 2000 23:09:25 +0200 | wenzelm | replaced infix Plus by <+>; | changeset | files |
| Thu, 13 Jul 2000 23:09:03 +0200 | wenzelm | removed duplicate Compl_atMost; | changeset | files |
| Thu, 13 Jul 2000 23:08:42 +0200 | wenzelm | fixed compose decl; | changeset | files |
| Thu, 13 Jul 2000 23:08:20 +0200 | wenzelm | defs: (overloaded) option; | changeset | files |
| Thu, 13 Jul 2000 23:07:56 +0200 | wenzelm | method cases/induct: (opaque) option; | changeset | files |
| Thu, 13 Jul 2000 23:07:10 +0200 | wenzelm | defs (overloaded); | changeset | files |
| Thu, 13 Jul 2000 13:05:58 +0200 | paulson | removed now-redundant proof steps | changeset | files |
| Thu, 13 Jul 2000 13:04:48 +0200 | paulson | added an important default rule | changeset | files |
| Thu, 13 Jul 2000 13:02:20 +0200 | paulson | fixed a failing proof | changeset | files |
| Thu, 13 Jul 2000 13:00:22 +0200 | paulson | le_refl_iff as default rule | changeset | files |
| Thu, 13 Jul 2000 12:59:26 +0200 | paulson | removed needless premises | changeset | files |
| Thu, 13 Jul 2000 12:56:42 +0200 | paulson | AddIffs now available for FOL, ZF | changeset | files |
| Thu, 13 Jul 2000 11:44:02 +0200 | wenzelm | added simp_case_tac; | changeset | files |
| Thu, 13 Jul 2000 11:42:11 +0200 | wenzelm | use InductMethod.simp_case_tac; | changeset | files |
| Thu, 13 Jul 2000 11:41:40 +0200 | wenzelm | tuned; | changeset | files |
| Thu, 13 Jul 2000 11:41:06 +0200 | wenzelm | export thesisN separately; | changeset | files |
| Thu, 13 Jul 2000 11:40:49 +0200 | wenzelm | prep rhs in original context; | changeset | files |
| Thu, 13 Jul 2000 11:39:41 +0200 | wenzelm | RuleCases.make opaq; | changeset | files |
| Thu, 13 Jul 2000 11:39:22 +0200 | wenzelm | bind_skolem; | changeset | files |
| Thu, 13 Jul 2000 11:39:03 +0200 | wenzelm | invoke_case: bind_skolem; | changeset | files |
| Thu, 13 Jul 2000 11:38:42 +0200 | wenzelm | "_i" arguments now expected to have skolems already internalized; | changeset | files |
| Thu, 13 Jul 2000 11:36:57 +0200 | wenzelm | make: opaq flag; | changeset | files |
| Thu, 13 Jul 2000 11:36:29 +0200 | wenzelm | added internal, dest_internal; | changeset | files |
| Wed, 12 Jul 2000 16:44:34 +0200 | wenzelm | infix 'OF' is a version of 'MRS' with more appropriate argument order; | changeset | files |
| Wed, 12 Jul 2000 14:47:55 +0200 | kleing | about.html -> logics.html | changeset | files |
| Wed, 12 Jul 2000 14:47:34 +0200 | kleing | munich webserver is now sunbroy51 | changeset | files |
| Wed, 12 Jul 2000 14:46:28 +0200 | kleing | about -> logics, better access to online libraries | changeset | files |
| Mon, 10 Jul 2000 12:17:34 +0200 | paulson | removal of (harmless) circular definitions | changeset | files |
| Sun, 09 Jul 2000 16:01:42 +0200 | berghofe | Tuned proof. | changeset | files |
| Sat, 08 Jul 2000 19:14:43 +0200 | nipkow | Defs are now checked for circularity (if not overloaded). | changeset | files |
| Fri, 07 Jul 2000 21:51:52 +0200 | wenzelm | inter_sort: keep normal! | changeset | files |
| Fri, 07 Jul 2000 18:29:34 +0200 | nipkow | Tightened up check of types in constant defs. | changeset | files |
| Fri, 07 Jul 2000 18:27:47 +0200 | nipkow | added type classes to constant's type | changeset | files |
| Fri, 07 Jul 2000 17:15:17 +0200 | bauerg | skp; le; | changeset | files |
| Fri, 07 Jul 2000 16:48:12 +0200 | oheimb | added dependency caveat | changeset | files |
| Fri, 07 Jul 2000 16:47:56 +0200 | oheimb | added dependency caveat | changeset | files |
| Fri, 07 Jul 2000 16:46:02 +0200 | oheimb | added IMP/Examples.ML dependence | changeset | files |
| Thu, 06 Jul 2000 18:12:17 +0200 | wenzelm | tuned msgs; | changeset | files |
| Thu, 06 Jul 2000 18:11:48 +0200 | wenzelm | allow comment in more commands; | changeset | files |
| Thu, 06 Jul 2000 18:11:15 +0200 | wenzelm | Isabelle99-1; | changeset | files |
| Thu, 06 Jul 2000 15:58:40 +0200 | kleing | ADD -> IAdd | changeset | files |
| Thu, 06 Jul 2000 15:38:42 +0200 | nipkow | Removed some junk thms. | changeset | files |
| Thu, 06 Jul 2000 15:38:26 +0200 | nipkow | added zabs to arith_tac | changeset | files |
| Thu, 06 Jul 2000 15:38:00 +0200 | nipkow | Deleted list_case thms no subsumed by case_tac | changeset | files |
| Thu, 06 Jul 2000 15:36:59 +0200 | nipkow | Now two split thms for same constant at different types is allowed. | changeset | files |
| Thu, 06 Jul 2000 15:01:52 +0200 | paulson | removal of batch style, and tidying | changeset | files |
| Thu, 06 Jul 2000 13:35:40 +0200 | paulson | removal of batch style, and tidying | changeset | files |
| Thu, 06 Jul 2000 13:28:36 +0200 | paulson | removal of batch style, and tidying | changeset | files |
| Thu, 06 Jul 2000 13:11:32 +0200 | paulson | removal of batch style, and tidying | changeset | files |
| Thu, 06 Jul 2000 12:27:37 +0200 | bauerg | removed sorry; | changeset | files |
| Thu, 06 Jul 2000 12:27:36 +0200 | bauerg | removed sorry; | changeset | files |
| Thu, 06 Jul 2000 12:15:05 +0200 | kleing | new ADD instruction | changeset | files |
| Thu, 06 Jul 2000 11:24:09 +0200 | paulson | removal of batch style, and tidying | changeset | files |
| Thu, 06 Jul 2000 11:23:39 +0200 | paulson | fixed typos reported by Jeremy Dawson | changeset | files |
| Thu, 06 Jul 2000 10:10:50 +0200 | bauerg | added; | changeset | files |
| Thu, 06 Jul 2000 10:10:10 +0200 | bauerg | completed TYPES version of HahnBanach; | changeset | files |
| Thu, 06 Jul 2000 09:46:56 +0200 | nipkow | *** empty log message *** | changeset | files |
| Thu, 06 Jul 2000 00:09:45 +0200 | wenzelm | Compatibility file for Moscow ML 2.00; | changeset | files |
| Thu, 06 Jul 2000 00:09:12 +0200 | wenzelm | run Moscow ML 2.00 --- does not handle saved images (yet!?); | changeset | files |
| Thu, 06 Jul 2000 00:08:24 +0200 | wenzelm | Moscow ML 2.00 or later (experimental!); | changeset | files |