src/HOL/Quickcheck_Narrowing.thy
changeset 55676 fb46f1c379b5
parent 55147 bce3dbc11f95
child 56047 1f283d0a4966
     1.1 --- a/src/HOL/Quickcheck_Narrowing.thy	Sat Feb 22 22:06:10 2014 +0100
     1.2 +++ b/src/HOL/Quickcheck_Narrowing.thy	Sun Feb 23 10:33:43 2014 +0100
     1.3 @@ -14,8 +14,11 @@
     1.4  setup {* Code_Target.extend_target ("Haskell_Quickcheck", (Code_Haskell.target, I)) *}
     1.5  
     1.6  code_printing
     1.7 -  type_constructor typerep \<rightharpoonup> (Haskell_Quickcheck) "Typerep"
     1.8 -| constant Typerep.Typerep \<rightharpoonup> (Haskell_Quickcheck) "Typerep"
     1.9 +  code_module Typerep \<rightharpoonup> (Haskell_Quickcheck) {*
    1.10 +data Typerep = Typerep String [Typerep]
    1.11 +*}
    1.12 +| type_constructor typerep \<rightharpoonup> (Haskell_Quickcheck) "Typerep.Typerep"
    1.13 +| constant Typerep.Typerep \<rightharpoonup> (Haskell_Quickcheck) "Typerep.Typerep"
    1.14  | type_constructor integer \<rightharpoonup> (Haskell_Quickcheck) "Prelude.Int"
    1.15  
    1.16  code_reserved Haskell_Quickcheck Typerep