src/HOL/Quickcheck_Narrowing.thy
changeset 52435 6646bb548c6b
parent 51143 0a2371e7ced3
child 55147 bce3dbc11f95
     1.1 --- a/src/HOL/Quickcheck_Narrowing.thy	Sun Jun 23 21:16:06 2013 +0200
     1.2 +++ b/src/HOL/Quickcheck_Narrowing.thy	Sun Jun 23 21:16:07 2013 +0200
     1.3 @@ -13,14 +13,10 @@
     1.4  
     1.5  setup {* Code_Target.extend_target ("Haskell_Quickcheck", (Code_Haskell.target, K I)) *}
     1.6  
     1.7 -code_type typerep
     1.8 -  (Haskell_Quickcheck "Typerep")
     1.9 -
    1.10 -code_const Typerep.Typerep
    1.11 -  (Haskell_Quickcheck "Typerep")
    1.12 -
    1.13 -code_type integer
    1.14 -  (Haskell_Quickcheck "Prelude.Int")
    1.15 +code_printing
    1.16 +  type_constructor typerep \<rightharpoonup> (Haskell_Quickcheck) "Typerep"
    1.17 +| constant Typerep.Typerep \<rightharpoonup> (Haskell_Quickcheck) "Typerep"
    1.18 +| type_constructor integer \<rightharpoonup> (Haskell_Quickcheck) "Prelude.Int"
    1.19  
    1.20  code_reserved Haskell_Quickcheck Typerep
    1.21  
    1.22 @@ -47,19 +43,19 @@
    1.23  
    1.24  consts nth :: "'a list => integer => 'a"
    1.25  
    1.26 -code_const nth (Haskell_Quickcheck infixl 9  "!!")
    1.27 +code_printing constant nth \<rightharpoonup> (Haskell_Quickcheck) infixl 9 "!!"
    1.28  
    1.29  consts error :: "char list => 'a"
    1.30  
    1.31 -code_const error (Haskell_Quickcheck "error")
    1.32 +code_printing constant error \<rightharpoonup> (Haskell_Quickcheck) "error"
    1.33  
    1.34  consts toEnum :: "integer => char"
    1.35  
    1.36 -code_const toEnum (Haskell_Quickcheck "Prelude.toEnum")
    1.37 +code_printing constant toEnum \<rightharpoonup> (Haskell_Quickcheck) "Prelude.toEnum"
    1.38  
    1.39  consts marker :: "char"
    1.40  
    1.41 -code_const marker (Haskell_Quickcheck "''\\0'")
    1.42 +code_printing constant marker \<rightharpoonup> (Haskell_Quickcheck) "''\\0'"
    1.43  
    1.44  subsubsection {* Narrowing's basic operations *}
    1.45