src/HOL/Lex/Chopper.thy

--- a/src/HOL/Lex/Chopper.thy	Wed Mar 03 22:58:23 2004 +0100
+++ b/src/HOL/Lex/Chopper.thy	Thu Mar 04 10:04:42 2004 +0100
@@ -15,13 +15,13 @@
 i.e. a set of strings.
 *)
 
-Chopper = List_Prefix +
+theory Chopper = List_Prefix:
 
-types   'a chopper = "'a list => 'a list list * 'a list"
+types 'a chopper = "'a list => 'a list list * 'a list"
 
 constdefs
-  is_longest_prefix_chopper :: ['a list => bool, 'a chopper] => bool
-  "is_longest_prefix_chopper L chopper == !xs.
+  is_longest_prefix_chopper :: "('a list => bool) => 'a chopper => bool"
+ "is_longest_prefix_chopper L chopper == !xs.
        (!zs. chopper(xs) = ([],zs) -->
              zs=xs & (!ys. ys ~= [] & ys <= xs --> ~L(ys))) &
        (!ys yss zs. chopper(xs) = (ys#yss,zs) -->