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.
merged
authorwenzelm
Mon, 22 Sep 2014 10:55:51 +0200
changeset 58416 d94ec306b7a8
parent 58414 f945e7af0d27 (diff)
parent 58415 8392d221bd91 (current diff)
child 58417 fa50722ad6cb
child 58418 a04b242a7a01
merged
--- a/src/HOL/Codegenerator_Test/Code_Test_GHC.thy	Mon Sep 22 10:18:41 2014 +0200
+++ b/src/HOL/Codegenerator_Test/Code_Test_GHC.thy	Mon Sep 22 10:55:51 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