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