src/HOL/String.thy
changeset 45182 10202ca034b0
parent 44278 1220ecb81e8f
child 45490 20c8c0cca555
     1.1 --- a/src/HOL/String.thy	Wed Oct 19 08:37:27 2011 +0200
     1.2 +++ b/src/HOL/String.thy	Wed Oct 19 08:37:29 2011 +0200
     1.3 @@ -213,31 +213,6 @@
     1.4    (Haskell infix 4 "==")
     1.5    (Scala infixl 5 "==")
     1.6  
     1.7 -types_code
     1.8 -  "char" ("string")
     1.9 -attach (term_of) {*
    1.10 -val term_of_char = HOLogic.mk_char o ord;
    1.11 -*}
    1.12 -attach (test) {*
    1.13 -fun gen_char i =
    1.14 -  let val j = random_range (ord "a") (Int.min (ord "a" + i, ord "z"))
    1.15 -  in (chr j, fn () => HOLogic.mk_char j) end;
    1.16 -*}
    1.17 -
    1.18 -setup {*
    1.19 -let
    1.20 -
    1.21 -fun char_codegen thy mode defs dep thyname b t gr =
    1.22 -  let
    1.23 -    val i = HOLogic.dest_char t;
    1.24 -    val (_, gr') = Codegen.invoke_tycodegen thy mode defs dep thyname false
    1.25 -      (fastype_of t) gr;
    1.26 -  in SOME (Codegen.str (ML_Syntax.print_string (chr i)), gr')
    1.27 -  end handle TERM _ => NONE;
    1.28 -
    1.29 -in Codegen.add_codegen "char_codegen" char_codegen end
    1.30 -*}
    1.31 -
    1.32  hide_type (open) literal
    1.33  
    1.34  end