Mercurial Mercurial > wneuper > isa / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
src/HOL/Library/Code_Char.thy
changeset 43092 bc1891226d00
parent 39499 0b61951d2682
child 43176 12635bb655fd
equal deleted inserted replaced
43091:594480d25aaa 43092: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
wneuper/isa