src/HOL/Lex/AutoChopper.thy
changeset 1374 5e407f2a3323
parent 1365 0defae128e43
child 1476 608483c2122a
     1.1 --- a/src/HOL/Lex/AutoChopper.thy	Wed Nov 29 16:58:30 1995 +0100
     1.2 +++ b/src/HOL/Lex/AutoChopper.thy	Wed Nov 29 17:01:41 1995 +0100
     1.3 @@ -17,8 +17,8 @@
     1.4  AutoChopper = Auto + Chopper +
     1.5  
     1.6  consts
     1.7 -  is_auto_chopper :: "(('a,'b)auto => 'a chopper) => bool"
     1.8 -  auto_chopper :: "('a,'b)auto => 'a chopper"
     1.9 +  is_auto_chopper :: (('a,'b)auto => 'a chopper) => bool
    1.10 +  auto_chopper :: ('a,'b)auto => 'a chopper
    1.11    acc :: "['a list, 'b, 'a list, 'a list, 'a list list*'a list, ('a,'b)auto]
    1.12  	  => 'a list list * 'a list"
    1.13