src/HOL/String.thy
author wenzelm
Sat Dec 23 22:50:19 2000 +0100 (2000-12-23)
changeset 10732 d4fda7d05ce5
parent 7224 e41e64476f9b
child 10909 2bbb1797bbe2
permissions -rw-r--r--
Tools/string_syntax.ML;
wenzelm@5121
     1
(*  Title:      HOL/String.thy
wenzelm@5121
     2
    ID:         $Id$
wenzelm@10732
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@10732
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
wenzelm@5121
     5
wenzelm@5121
     6
Hex chars and strings.
wenzelm@5121
     7
*)
wenzelm@5121
     8
wenzelm@10732
     9
theory String = List
wenzelm@10732
    10
files "Tools/string_syntax.ML":
wenzelm@5121
    11
wenzelm@10732
    12
datatype nibble =
wenzelm@10732
    13
    H00 | H01 | H02 | H03 | H04 | H05 | H06 | H07
wenzelm@10732
    14
  | H08 | H09 | H0A | H0B | H0C | H0D | H0E | H0F
wenzelm@5121
    15
wenzelm@10732
    16
datatype char = Char nibble nibble
wenzelm@10732
    17
types string = "char list"
wenzelm@5121
    18
wenzelm@5121
    19
syntax
wenzelm@10732
    20
  "_Char" :: "xstr => char"    ("CHR _")
wenzelm@10732
    21
  "_String" :: "xstr => string"    ("_")
wenzelm@10732
    22
wenzelm@10732
    23
setup StringSyntax.setup
wenzelm@5121
    24
wenzelm@5121
    25
end