slight adaption for code generator
authorhaftmann
Wed Jun 14 12:14:42 2006 +0200 (2006-06-14)
changeset 198901aad48bcc674
parent 19889 2202a5648897
child 19891 2857fac35e6d
slight adaption for code generator
src/HOL/Datatype.thy
src/HOL/HOL.thy
src/HOL/Lambda/WeakNorm.thy
src/HOL/List.thy
src/HOL/Nat.thy
src/HOL/Wellfounded_Recursion.thy
     1.1 --- a/src/HOL/Datatype.thy	Wed Jun 14 12:14:13 2006 +0200
     1.2 +++ b/src/HOL/Datatype.thy	Wed Jun 14 12:14:42 2006 +0200
     1.3 @@ -257,14 +257,11 @@
     1.4    fst_conv [code]
     1.5    snd_conv [code]
     1.6  
     1.7 -lemma [code unfolt]:
     1.8 -  "1 == Suc 0" by simp
     1.9 -
    1.10 -code_syntax_tyco bool
    1.11 +code_typapp bool
    1.12    ml (target_atom "bool")
    1.13    haskell (target_atom "Bool")
    1.14  
    1.15 -code_syntax_const
    1.16 +code_constapp
    1.17    True
    1.18      ml (target_atom "true")
    1.19      haskell (target_atom "True")
    1.20 @@ -284,32 +281,32 @@
    1.21      ml (target_atom "(if __/ then __/ else __)")
    1.22      haskell (target_atom "(if __/ then __/ else __)")
    1.23  
    1.24 -code_syntax_tyco
    1.25 +code_typapp
    1.26    *
    1.27      ml (infix 2 "*")
    1.28      haskell (target_atom "(__,/ __)")
    1.29  
    1.30 -code_syntax_const
    1.31 +code_constapp
    1.32    Pair
    1.33      ml (target_atom "(__,/ __)")
    1.34      haskell (target_atom "(__,/ __)")
    1.35  
    1.36 -code_syntax_tyco
    1.37 +code_typapp
    1.38    unit
    1.39      ml (target_atom "unit")
    1.40      haskell (target_atom "()")
    1.41  
    1.42 -code_syntax_const
    1.43 +code_constapp
    1.44    Unity
    1.45      ml (target_atom "()")
    1.46      haskell (target_atom "()")
    1.47  
    1.48 -code_syntax_tyco
    1.49 +code_typapp
    1.50    option
    1.51      ml ("_ option")
    1.52      haskell ("Maybe _")
    1.53  
    1.54 -code_syntax_const
    1.55 +code_constapp
    1.56    None
    1.57      ml (target_atom "NONE")
    1.58      haskell (target_atom "Nothing")
     2.1 --- a/src/HOL/HOL.thy	Wed Jun 14 12:14:13 2006 +0200
     2.2 +++ b/src/HOL/HOL.thy	Wed Jun 14 12:14:42 2006 +0200
     2.3 @@ -1412,7 +1412,7 @@
     2.4    Not "HOL.not"
     2.5    arbitrary "HOL.arbitrary"
     2.6  
     2.7 -code_syntax_const
     2.8 +code_constapp
     2.9    "op =" (* an intermediate solution for polymorphic equality *)
    2.10      ml (infixl 6 "=")
    2.11      haskell (infixl 4 "==")
     3.1 --- a/src/HOL/Lambda/WeakNorm.thy	Wed Jun 14 12:14:13 2006 +0200
     3.2 +++ b/src/HOL/Lambda/WeakNorm.thy	Wed Jun 14 12:14:42 2006 +0200
     3.3 @@ -501,7 +501,7 @@
     3.4    arbitrary :: "'a"       ("(error \"arbitrary\")")
     3.5    arbitrary :: "'a \<Rightarrow> 'b" ("(fn '_ => error \"arbitrary\")")
     3.6  
     3.7 -code_syntax_const
     3.8 +code_constapp
     3.9    "arbitrary :: 'a"       ml (target_atom "(error \"arbitrary\")")
    3.10    "arbitrary :: 'a \<Rightarrow> 'b" ml (target_atom "(fn '_ => error \"arbitrary\")")
    3.11  
     4.1 --- a/src/HOL/List.thy	Wed Jun 14 12:14:13 2006 +0200
     4.2 +++ b/src/HOL/List.thy	Wed Jun 14 12:14:42 2006 +0200
     4.3 @@ -2737,17 +2737,17 @@
     4.4    "List.op @" "List.append"
     4.5    "List.op mem" "List.mem"
     4.6  
     4.7 -code_syntax_tyco
     4.8 +code_typapp
     4.9    list
    4.10      ml ("_ list")
    4.11      haskell (target_atom "[_]")
    4.12  
    4.13 -code_syntax_const
    4.14 +code_constapp
    4.15    Nil
    4.16      ml (target_atom "[]")
    4.17      haskell (target_atom "[]")
    4.18  
    4.19 -code_syntax_tyco
    4.20 +code_typapp
    4.21    char
    4.22      ml (target_atom "char")
    4.23      haskell (target_atom "Char")
     5.1 --- a/src/HOL/Nat.thy	Wed Jun 14 12:14:13 2006 +0200
     5.2 +++ b/src/HOL/Nat.thy	Wed Jun 14 12:14:42 2006 +0200
     5.3 @@ -601,7 +601,8 @@
     5.4  lemma add_Suc_right [simp]: "m + Suc n = Suc (m + n)"
     5.5    by (induct m) simp_all
     5.6  
     5.7 -lemma [code]: "Suc m + n = m + Suc n" by simp
     5.8 +lemma add_Suc_shift [code]: "Suc m + n = m + Suc n"
     5.9 +  by simp
    5.10  
    5.11  
    5.12  text {* Associative law for addition *}
     6.1 --- a/src/HOL/Wellfounded_Recursion.thy	Wed Jun 14 12:14:13 2006 +0200
     6.2 +++ b/src/HOL/Wellfounded_Recursion.thy	Wed Jun 14 12:14:42 2006 +0200
     6.3 @@ -295,7 +295,7 @@
     6.4    CodegenPackage.add_appconst ("wfrec", ((3, 3), CodegenPackage.appgen_wfrec))
     6.5  *}
     6.6  
     6.7 -code_syntax_const
     6.8 +code_constapp
     6.9    wfrec
    6.10      ml ("let fun wfrec f x = f (wfrec f) x in wfrec _ _ end;")
    6.11      haskell ("wfrec _ _ where wfrec f x = f (wfrec f) x")