Wed, 12 Feb 2014 09:06:04 +0100 | Andreas Lochbihler | make integer_of_char and char_of_integer work with NBE and code_simp | changeset | files |
Wed, 12 Feb 2014 08:56:38 +0100 | Andreas Lochbihler | make lifting setup for String.literal local to prevent transfer from replacing STR ''...'' literals | changeset | files |
Wed, 12 Feb 2014 10:20:31 +0100 | blanchet | [mq]: news | changeset | files |
Wed, 12 Feb 2014 08:37:28 +0100 | blanchet | remove hidden fact about hidden constant from code generator setup | changeset | files |
Wed, 12 Feb 2014 08:37:28 +0100 | blanchet | for extraction -- use the exhaust rule that's registered with 'datatype_realizer.ML' | changeset | files |
Wed, 12 Feb 2014 08:37:28 +0100 | blanchet | compile | changeset | files |