src/HOL/Lex/Prefix.thy
changeset 8523 7ffc94f2f42d
parent 6675 63e53327f5e5
child 9156 b9fe44ad3381
equal deleted inserted replaced
8522:581dfabf22dd 8523:7ffc94f2f42d
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     3     Author:     Tobias Nipkow
     4     Copyright   1995 TUM
     4     Copyright   1995 TUM
     5 *)
     5 *)
     6 
     6 
     7 Prefix = List +
     7 Prefix = Main +
     8 
     8 
     9 arities list :: (term)ord
     9 arities list :: (term)ord
    10 
    10 
    11 defs
    11 defs
    12         prefix_def        "xs <= zs  ==  ? ys. zs = xs@ys"
    12         prefix_def        "xs <= zs  ==  ? ys. zs = xs@ys"