| Wed, 15 Sep 2010 16:47:31 +0200 | haftmann | introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy | changeset | files |
| Wed, 15 Sep 2010 17:05:18 +0200 | blanchet | merged | changeset | files |
| Wed, 15 Sep 2010 16:23:11 +0200 | blanchet | "Metis." -> "Metis_" to reflect change in "metis.ML" | changeset | files |
| Wed, 15 Sep 2010 16:22:02 +0200 | blanchet | no need for "metis_env.ML" anymore; | changeset | files |
| Wed, 15 Sep 2010 16:20:46 +0200 | blanchet | regenerate "metis.ML", this time without manual hacks | changeset | files |
| Wed, 15 Sep 2010 16:19:49 +0200 | blanchet | remove needless file for us | changeset | files |
| Wed, 15 Sep 2010 16:17:05 +0200 | blanchet | got rid of three crude regexps from "make_metis" | changeset | files |
| Wed, 15 Sep 2010 16:16:33 +0200 | blanchet | more Isabelle-specific changes | changeset | files |