Wed, 15 Sep 2010 16:56:31 +0200 | haftmann | proper interface for code_reflect | changeset | files |
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 |