src/HOL/ex/Codegenerator.thy
changeset 21125 9b7d35ca1eef
parent 21092 2e0a59d829d5
child 21155 95142d816793
     1.1 --- a/src/HOL/ex/Codegenerator.thy	Tue Oct 31 09:29:18 2006 +0100
     1.2 +++ b/src/HOL/ex/Codegenerator.thy	Tue Oct 31 14:58:12 2006 +0100
     1.3 @@ -5,7 +5,7 @@
     1.4  header {* Test and Examples for code generator *}
     1.5  
     1.6  theory Codegenerator
     1.7 -imports Main Records
     1.8 +imports Main (*"~/projects/codegen/thy/CodegenSetup"*) Records
     1.9  begin
    1.10  
    1.11  subsection {* booleans *}
    1.12 @@ -197,7 +197,7 @@
    1.13    "Code_Generator.eq :: mut2 \<Rightarrow> mut2 \<Rightarrow> bool"
    1.14    "Code_Generator.eq :: ('a\<Colon>eq) point_scheme \<Rightarrow> 'a point_scheme \<Rightarrow> bool"
    1.15  
    1.16 -code_gen (SML -)
    1.17 +code_gen (SML *)
    1.18  code_gen (Haskell -)
    1.19  
    1.20  end
    1.21 \ No newline at end of file