| changeset 1374 | 5e407f2a3323 |
| parent 1344 | f172a7f14e49 |
| child 1476 | 608483c2122a |
--- a/src/HOL/Lex/Chopper.thy Wed Nov 29 16:58:30 1995 +0100 +++ b/src/HOL/Lex/Chopper.thy Wed Nov 29 17:01:41 1995 +0100 @@ -20,7 +20,7 @@ types 'a chopper = "'a list => 'a list list * 'a list" consts - is_longest_prefix_chopper :: "['a list => bool, 'a chopper] => bool" + is_longest_prefix_chopper :: ['a list => bool, 'a chopper] => bool defs is_longest_prefix_chopper_def