| Sun, 27 Nov 2005 05:00:43 +0100 | urbanc | added the version of nominal.thy that contains | changeset | files |
| Sun, 27 Nov 2005 04:59:20 +0100 | urbanc | cleaned up all examples so that they work with the | changeset | files |
| Sun, 27 Nov 2005 03:55:16 +0100 | urbanc | finished cleaning up the parts that collect | changeset | files |
| Sat, 26 Nov 2005 18:41:41 +0100 | berghofe | Corrected treatment of non-recursive abstraction types. | changeset | files |
| Fri, 25 Nov 2005 21:14:34 +0100 | wenzelm | tuned induct proofs; | changeset | files |
| Fri, 25 Nov 2005 20:57:51 +0100 | wenzelm | induct: insert defs in object-logic form; | changeset | files |
| Fri, 25 Nov 2005 19:20:56 +0100 | wenzelm | tuned induct proofs; | changeset | files |
| Fri, 25 Nov 2005 19:09:44 +0100 | wenzelm | tuned induct proofs; | changeset | files |
| Fri, 25 Nov 2005 18:58:43 +0100 | wenzelm | consume: unfold defs in all major prems; | changeset | files |
| Fri, 25 Nov 2005 18:58:42 +0100 | wenzelm | revert_skolem: fall back on Syntax.deskolem; | changeset | files |
| Fri, 25 Nov 2005 18:58:41 +0100 | wenzelm | forall_conv ~1; | changeset | files |
| Fri, 25 Nov 2005 18:58:40 +0100 | wenzelm | added dummy_pattern; | changeset | files |
| Fri, 25 Nov 2005 18:58:38 +0100 | wenzelm | tuned names; | changeset | files |
| Fri, 25 Nov 2005 18:58:37 +0100 | wenzelm | forall_conv: limit prefix; | changeset | files |
| Fri, 25 Nov 2005 18:58:36 +0100 | wenzelm | fix_tac: proper treatment of major premises in goal; | changeset | files |
| Fri, 25 Nov 2005 18:58:35 +0100 | wenzelm | removed obsolete dummy paragraphs; | changeset | files |
| Fri, 25 Nov 2005 18:58:34 +0100 | wenzelm | tuned; | changeset | files |
| Fri, 25 Nov 2005 17:41:52 +0100 | haftmann | code generator: case expressions, improved name resolving | changeset | files |
| Fri, 25 Nov 2005 14:51:39 +0100 | urbanc | added fsub.thy (poplmark challenge) to the examples | changeset | files |
| Fri, 25 Nov 2005 14:00:22 +0100 | berghofe | Fixed problem with strong induction theorem for datatypes containing | changeset | files |
| Fri, 25 Nov 2005 11:34:37 +0100 | kleing | send more information with test-takes-too-long message | changeset | files |
| Thu, 24 Nov 2005 12:14:56 +0100 | wenzelm | fixed spelling of 'case_conclusion'; | changeset | files |
| Thu, 24 Nov 2005 00:00:20 +0100 | wenzelm | tuned induct proofs; | changeset | files |
| Wed, 23 Nov 2005 22:26:13 +0100 | wenzelm | tuned induction proofs; | changeset | files |
| Wed, 23 Nov 2005 22:23:52 +0100 | wenzelm | more robust revert_skolem; | changeset | files |
| Wed, 23 Nov 2005 20:29:36 +0100 | wenzelm | tuned; | changeset | files |
| Wed, 23 Nov 2005 18:52:05 +0100 | wenzelm | Provers/induct: definitional insts and fixing; | changeset | files |
| Wed, 23 Nov 2005 18:52:04 +0100 | wenzelm | consume: proper treatment of defs; | changeset | files |
| Wed, 23 Nov 2005 18:52:03 +0100 | wenzelm | added case_conclusion attribute; | changeset | files |
| Wed, 23 Nov 2005 18:52:02 +0100 | wenzelm | (co)induct: taking; | changeset | files |
| Wed, 23 Nov 2005 18:52:01 +0100 | wenzelm | RuleCases.case_conclusion; | changeset | files |
| Wed, 23 Nov 2005 18:52:00 +0100 | wenzelm | tuned; | changeset | files |
| Wed, 23 Nov 2005 18:51:59 +0100 | wenzelm | added case_conclusion attribute; | changeset | files |
| Wed, 23 Nov 2005 17:16:42 +0100 | haftmann | improved failure tracking | changeset | files |
| Tue, 22 Nov 2005 19:37:36 +0100 | wenzelm | Datatype_Universe: hide base names only; | changeset | files |
| Tue, 22 Nov 2005 19:34:50 +0100 | wenzelm | added type cases/cases_tactic, and CASES, SUBGOAL_CASES; | changeset | files |
| Tue, 22 Nov 2005 19:34:48 +0100 | wenzelm | cases_tactic; | changeset | files |
| Tue, 22 Nov 2005 19:34:47 +0100 | wenzelm | moved multi_resolve(s) to drule.ML; | changeset | files |
| Tue, 22 Nov 2005 19:34:46 +0100 | wenzelm | find_xxxS: term instead of thm; | changeset | files |
| Tue, 22 Nov 2005 19:34:44 +0100 | wenzelm | export map_tags; | changeset | files |
| Tue, 22 Nov 2005 19:34:43 +0100 | wenzelm | make coinduct actually work; | changeset | files |
| Tue, 22 Nov 2005 19:34:41 +0100 | wenzelm | Drule.multi_resolves; | changeset | files |
| Tue, 22 Nov 2005 19:34:40 +0100 | wenzelm | declare coinduct rule; | changeset | files |
| Tue, 22 Nov 2005 14:32:01 +0100 | haftmann | added code generator syntax | changeset | files |
| Tue, 22 Nov 2005 12:59:25 +0100 | haftmann | added codegenerator | changeset | files |
| Tue, 22 Nov 2005 12:42:59 +0100 | haftmann | added code generator syntax | changeset | files |
| Tue, 22 Nov 2005 10:09:11 +0100 | paulson | new treatment of polymorphic types, using Sign.const_typargs | changeset | files |
| Mon, 21 Nov 2005 16:51:57 +0100 | haftmann | added codegen package | changeset | files |
| Mon, 21 Nov 2005 15:15:32 +0100 | haftmann | added serializer | changeset | files |
| Mon, 21 Nov 2005 11:14:11 +0100 | paulson | tweak | changeset | files |
| Mon, 21 Nov 2005 10:44:14 +0100 | haftmann | fixed some inconveniencies in website | changeset | files |
| Sat, 19 Nov 2005 14:22:28 +0100 | wenzelm | CONJUNCTS; | changeset | files |
| Sat, 19 Nov 2005 14:21:09 +0100 | wenzelm | tuned; | changeset | files |
| Sat, 19 Nov 2005 14:21:08 +0100 | wenzelm | Goal.norm_hhf_protected; | changeset | files |
| Sat, 19 Nov 2005 14:21:07 +0100 | wenzelm | added coinduct attribute; | changeset | files |
| Sat, 19 Nov 2005 14:21:06 +0100 | wenzelm | added CONJUNCTS: treat conjunction as separate sub-goals; | changeset | files |
| Sat, 19 Nov 2005 14:21:05 +0100 | wenzelm | simpset: added reorient field, set_reorient; | changeset | files |
| Sat, 19 Nov 2005 14:21:04 +0100 | wenzelm | tuned norm_hhf_protected; | changeset | files |
| Sat, 19 Nov 2005 14:21:03 +0100 | wenzelm | removed conj_mono; | changeset | files |
| Sat, 19 Nov 2005 14:21:02 +0100 | wenzelm | induct: CONJUNCTS for multiple goals; | changeset | files |