src/HOL/Lex/Prefix.thy
author paulson
Mon, 20 Mar 2000 10:24:07 +0100
changeset 8523 7ffc94f2f42d
parent 6675 63e53327f5e5
child 9156 b9fe44ad3381
permissions -rw-r--r--
now based on "Main", as it should be
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1344
diff changeset
     1
(*  Title:      HOL/Lex/Prefix.thy
1344
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
     2
    ID:         $Id$
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1344
diff changeset
     3
    Author:     Tobias Nipkow
1344
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
     4
    Copyright   1995 TUM
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
     5
*)
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
     6
8523
7ffc94f2f42d now based on "Main", as it should be
paulson
parents: 6675
diff changeset
     7
Prefix = Main +
1344
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
     8
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
     9
arities list :: (term)ord
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
    10
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
    11
defs
6675
63e53327f5e5 changes to show that Lists are partially ordered by the prefix relation
paulson
parents: 1476
diff changeset
    12
        prefix_def        "xs <= zs  ==  ? ys. zs = xs@ys"
63e53327f5e5 changes to show that Lists are partially ordered by the prefix relation
paulson
parents: 1476
diff changeset
    13
63e53327f5e5 changes to show that Lists are partially ordered by the prefix relation
paulson
parents: 1476
diff changeset
    14
        strict_prefix_def "xs < zs  ==  xs <= zs & xs ~= (zs::'a list)"
63e53327f5e5 changes to show that Lists are partially ordered by the prefix relation
paulson
parents: 1476
diff changeset
    15
  
1344
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
    16
end