src/HOL/Library/LSC.thy
changeset 41909 383bbdad1650
parent 41908 3bd9a21366d2
child 41910 709c04e7b703
equal deleted inserted replaced
41908:3bd9a21366d2 41909:383bbdad1650
     6 imports Main "~~/src/HOL/Library/Code_Char"
     6 imports Main "~~/src/HOL/Library/Code_Char"
     7 uses ("~~/src/HOL/Tools/LSC/lazysmallcheck.ML")
     7 uses ("~~/src/HOL/Tools/LSC/lazysmallcheck.ML")
     8 begin
     8 begin
     9 
     9 
    10 subsection {* Counterexample generator *}
    10 subsection {* Counterexample generator *}
       
    11 
       
    12 subsubsection {* Code generation setup *}
       
    13 
       
    14 code_type typerep
       
    15   ("Haskell" "Typerep")
       
    16 
       
    17 code_const Typerep.Typerep
       
    18   ("Haskell" "Typerep")
       
    19 
       
    20 code_reserved Haskell Typerep
    11 
    21 
    12 subsubsection {* Type code_int for Haskell's Int type *}
    22 subsubsection {* Type code_int for Haskell's Int type *}
    13 
    23 
    14 typedef (open) code_int = "UNIV \<Colon> int set"
    24 typedef (open) code_int = "UNIV \<Colon> int set"
    15   morphisms int_of of_int by rule
    25   morphisms int_of of_int by rule