src/HOL/ex/Codegenerator.thy
changeset 21046 fe1db2f991a7
parent 20968 5294baa98468
child 21080 7d73aa966207
     1.1 --- a/src/HOL/ex/Codegenerator.thy	Mon Oct 16 14:07:21 2006 +0200
     1.2 +++ b/src/HOL/ex/Codegenerator.thy	Mon Oct 16 14:07:31 2006 +0200
     1.3 @@ -184,16 +184,16 @@
     1.4    "op mod :: int \<Rightarrow> int \<Rightarrow> int"  
     1.5    (SML) (Haskell)
     1.6  code_gen
     1.7 -  "OperationalEquality.eq :: bool \<Rightarrow> bool \<Rightarrow> bool"
     1.8 -  "OperationalEquality.eq :: nat \<Rightarrow> nat \<Rightarrow> bool"
     1.9 -  "OperationalEquality.eq :: int \<Rightarrow> int \<Rightarrow> bool"
    1.10 -  "OperationalEquality.eq :: ('a\<Colon>eq) * ('b\<Colon>eq) \<Rightarrow> 'a * 'b \<Rightarrow> bool"
    1.11 -  "OperationalEquality.eq :: ('a\<Colon>eq) + ('b\<Colon>eq) \<Rightarrow> 'a + 'b \<Rightarrow> bool"
    1.12 -  "OperationalEquality.eq :: ('a\<Colon>eq) option \<Rightarrow> 'a option \<Rightarrow> bool"
    1.13 -  "OperationalEquality.eq :: ('a\<Colon>eq) list \<Rightarrow> 'a list \<Rightarrow> bool"
    1.14 -  "OperationalEquality.eq :: mut1 \<Rightarrow> mut1 \<Rightarrow> bool"
    1.15 -  "OperationalEquality.eq :: mut2 \<Rightarrow> mut2 \<Rightarrow> bool"
    1.16 -  "OperationalEquality.eq :: ('a\<Colon>eq) point_scheme \<Rightarrow> 'a point_scheme \<Rightarrow> bool"
    1.17 +  "Code_Generator.eq :: bool \<Rightarrow> bool \<Rightarrow> bool"
    1.18 +  "Code_Generator.eq :: nat \<Rightarrow> nat \<Rightarrow> bool"
    1.19 +  "Code_Generator.eq :: int \<Rightarrow> int \<Rightarrow> bool"
    1.20 +  "Code_Generator.eq :: ('a\<Colon>eq) * ('b\<Colon>eq) \<Rightarrow> 'a * 'b \<Rightarrow> bool"
    1.21 +  "Code_Generator.eq :: ('a\<Colon>eq) + ('b\<Colon>eq) \<Rightarrow> 'a + 'b \<Rightarrow> bool"
    1.22 +  "Code_Generator.eq :: ('a\<Colon>eq) option \<Rightarrow> 'a option \<Rightarrow> bool"
    1.23 +  "Code_Generator.eq :: ('a\<Colon>eq) list \<Rightarrow> 'a list \<Rightarrow> bool"
    1.24 +  "Code_Generator.eq :: mut1 \<Rightarrow> mut1 \<Rightarrow> bool"
    1.25 +  "Code_Generator.eq :: mut2 \<Rightarrow> mut2 \<Rightarrow> bool"
    1.26 +  "Code_Generator.eq :: ('a\<Colon>eq) point_scheme \<Rightarrow> 'a point_scheme \<Rightarrow> bool"
    1.27  
    1.28  code_gen (SML -)
    1.29