src/HOL/ex/Codegenerator.thy
changeset 21460 cda5cd8bfd16
parent 21420 8b15e5e66813
child 21511 16c62deb1adf
     1.1 --- a/src/HOL/ex/Codegenerator.thy	Wed Nov 22 10:20:19 2006 +0100
     1.2 +++ b/src/HOL/ex/Codegenerator.thy	Wed Nov 22 10:20:20 2006 +0100
     1.3 @@ -179,16 +179,16 @@
     1.4    "op mod :: int \<Rightarrow> int \<Rightarrow> int"  
     1.5    (SML) (Haskell)
     1.6  code_gen
     1.7 -  "Code_Generator.eq :: bool \<Rightarrow> bool \<Rightarrow> bool"
     1.8 -  "Code_Generator.eq :: nat \<Rightarrow> nat \<Rightarrow> bool"
     1.9 -  "Code_Generator.eq :: int \<Rightarrow> int \<Rightarrow> bool"
    1.10 -  "Code_Generator.eq :: ('a\<Colon>eq) * ('b\<Colon>eq) \<Rightarrow> 'a * 'b \<Rightarrow> bool"
    1.11 -  "Code_Generator.eq :: ('a\<Colon>eq) + ('b\<Colon>eq) \<Rightarrow> 'a + 'b \<Rightarrow> bool"
    1.12 -  "Code_Generator.eq :: ('a\<Colon>eq) option \<Rightarrow> 'a option \<Rightarrow> bool"
    1.13 -  "Code_Generator.eq :: ('a\<Colon>eq) list \<Rightarrow> 'a list \<Rightarrow> bool"
    1.14 -  "Code_Generator.eq :: mut1 \<Rightarrow> mut1 \<Rightarrow> bool"
    1.15 -  "Code_Generator.eq :: mut2 \<Rightarrow> mut2 \<Rightarrow> bool"
    1.16 -  "Code_Generator.eq :: ('a\<Colon>eq) point_scheme \<Rightarrow> 'a point_scheme \<Rightarrow> bool"
    1.17 +  "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"
    1.18 +  "op = :: nat \<Rightarrow> nat \<Rightarrow> bool"
    1.19 +  "op = :: int \<Rightarrow> int \<Rightarrow> bool"
    1.20 +  "op = :: ('a\<Colon>eq) * ('b\<Colon>eq) \<Rightarrow> 'a * 'b \<Rightarrow> bool"
    1.21 +  "op = :: ('a\<Colon>eq) + ('b\<Colon>eq) \<Rightarrow> 'a + 'b \<Rightarrow> bool"
    1.22 +  "op = :: ('a\<Colon>eq) option \<Rightarrow> 'a option \<Rightarrow> bool"
    1.23 +  "op = :: ('a\<Colon>eq) list \<Rightarrow> 'a list \<Rightarrow> bool"
    1.24 +  "op = :: mut1 \<Rightarrow> mut1 \<Rightarrow> bool"
    1.25 +  "op = :: mut2 \<Rightarrow> mut2 \<Rightarrow> bool"
    1.26 +  "op = :: ('a\<Colon>eq) point_scheme \<Rightarrow> 'a point_scheme \<Rightarrow> bool"
    1.27  
    1.28  code_gen (SML *) (Haskell -)
    1.29