| Fri, 07 Dec 2007 15:07:54 +0100 | haftmann | dropped Instance.instantiate | changeset | files |
| Fri, 07 Dec 2007 10:59:03 +0100 | krauss | Adding "ex/Induction_Scheme.thy" to tests | changeset | files |
| Fri, 07 Dec 2007 09:42:20 +0100 | krauss | experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy) | changeset | files |
| Fri, 07 Dec 2007 08:38:50 +0100 | haftmann | tuned further | changeset | files |
| Thu, 06 Dec 2007 22:07:11 +0100 | wenzelm | renamed ML_PID to PID; | changeset | files |
| Thu, 06 Dec 2007 19:58:21 +0100 | nipkow | R&F: added sgn lemma | changeset | files |
| Thu, 06 Dec 2007 17:05:44 +0100 | haftmann | temporary code generator work arounds | changeset | files |
| Thu, 06 Dec 2007 16:56:00 +0100 | haftmann | fixed slip | changeset | files |
| Thu, 06 Dec 2007 16:38:42 +0100 | haftmann | -authentic primrec | changeset | files |
| Thu, 06 Dec 2007 16:36:21 +0100 | haftmann | dropped legacy bindings | changeset | files |
| Thu, 06 Dec 2007 16:36:19 +0100 | haftmann | authentic primrec | changeset | files |
| Thu, 06 Dec 2007 15:10:12 +0100 | haftmann | dropped void space | changeset | files |
| Thu, 06 Dec 2007 15:10:09 +0100 | haftmann | added new primrec package | changeset | files |
| Thu, 06 Dec 2007 12:58:01 +0100 | krauss | load sum_tree.ML | changeset | files |
| Thu, 06 Dec 2007 12:23:52 +0100 | krauss | factored out handling of sum types again | changeset | files |
| Thu, 06 Dec 2007 00:21:34 +0100 | wenzelm | added test_markup; | changeset | files |
| Thu, 06 Dec 2007 00:21:32 +0100 | wenzelm | moved basic test_markup to isabelle_process.ML; | changeset | files |
| Thu, 06 Dec 2007 00:21:32 +0100 | wenzelm | added channels; | changeset | files |
| Thu, 06 Dec 2007 00:21:30 +0100 | wenzelm | replaced Markup.enclose by Markup.markup, which operates on plain strings instead of raw output; | changeset | files |
| Thu, 06 Dec 2007 00:21:28 +0100 | wenzelm | check persistent sessions; | changeset | files |
| Wed, 05 Dec 2007 20:56:42 +0100 | wenzelm | tuned signature; | changeset | files |
| Wed, 05 Dec 2007 20:30:35 +0100 | wenzelm | made SML/NJ happy; | changeset | files |
| Wed, 05 Dec 2007 20:16:36 +0100 | wenzelm | removed -e flag from most sessions; | changeset | files |
| Wed, 05 Dec 2007 16:54:50 +0100 | obua | instance int,real :: lordered_ring | changeset | files |
| Wed, 05 Dec 2007 14:36:58 +0100 | krauss | methods "relation" and "lexicographic_order" do not insist on applying the "f.termination" rule of a function. | changeset | files |
| Wed, 05 Dec 2007 14:32:17 +0100 | haftmann | tuned class parts | changeset | files |
| Wed, 05 Dec 2007 14:16:15 +0100 | haftmann | dropped Classpackage.thy | changeset | files |
| Wed, 05 Dec 2007 14:16:14 +0100 | haftmann | tuned | changeset | files |
| Wed, 05 Dec 2007 14:16:13 +0100 | haftmann | added parser for multi_arity | changeset | files |
| Wed, 05 Dec 2007 14:16:12 +0100 | haftmann | added constrain_thm | changeset | files |