Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
drop workaround addressed by d0d3c30806b4
authorAndreas Lochbihler
Mon, 22 Sep 2014 10:53:54 +0200
changeset 58414 f945e7af0d27
parent 58413 22dd971f6938
child 58416 d94ec306b7a8
drop workaround addressed by d0d3c30806b4
src/HOL/Codegenerator_Test/Code_Test_GHC.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Codegenerator_Test/Code_Test_GHC.thy	Sun Sep 21 20:22:12 2014 +0200
+++ b/src/HOL/Codegenerator_Test/Code_Test_GHC.thy	Mon Sep 22 10:53:54 2014 +0200
@@ -6,9 +6,7 @@
 
 theory Code_Test_GHC imports Code_Test begin
 
-definition id_integer :: "integer \<Rightarrow> integer" where "id_integer = id"
-
-test_code "id_integer (14 + 7 * -12) = 140 div -2" in GHC
+test_code "(14 + 7 * -12 :: integer) = 140 div -2" in GHC
 
 value [GHC] "14 + 7 * -12 :: integer"
isabelle