author  paulson 
Fri, 21 May 1999 10:50:04 +0200  
changeset 6675  63e53327f5e5 
parent 1476  608483c2122a 
child 8523  7ffc94f2f42d 
permissions  rwrr 
1476  1 
(* Title: HOL/Lex/Prefix.thy 
1344  2 
ID: $Id$ 
1476  3 
Author: Tobias Nipkow 
1344  4 
Copyright 1995 TUM 
5 
*) 

6 

7 
Prefix = List + 

8 

9 
arities list :: (term)ord 

10 

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  16 
end 