src/HOL/Library/Code_Char.thy
changeset 42231 bc1891226d00
parent 39272 0b61951d2682
child 42316 12635bb655fd
equal deleted inserted replaced
42230:594480d25aaa 42231:bc1891226d00
    56   (SML "String.explode")
    56   (SML "String.explode")
    57   (OCaml "failwith/ \"explode\"")
    57   (OCaml "failwith/ \"explode\"")
    58   (Haskell "_")
    58   (Haskell "_")
    59   (Scala "!(_.toList)")
    59   (Scala "!(_.toList)")
    60 
    60 
       
    61 
       
    62 declare Quickcheck_Exhaustive.char.bounded_forall_char.simps [code del]
       
    63 
    61 end
    64 end