Wed, 15 Sep 2010 19:20:50 +0200 | haftmann | merged | changeset | files |
Wed, 15 Sep 2010 16:56:31 +0200 | haftmann | load code_runtime immediately again | changeset | files |
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 |