src/HOL/Lex/Auto.thy
changeset 1374 5e407f2a3323
parent 1344 f172a7f14e49
child 1476 608483c2122a
     1.1 --- a/src/HOL/Lex/Auto.thy	Wed Nov 29 16:58:30 1995 +0100
     1.2 +++ b/src/HOL/Lex/Auto.thy	Wed Nov 29 17:01:41 1995 +0100
     1.3 @@ -17,12 +17,12 @@
     1.4  types ('a,'b)auto = "'b * ('b => 'a => 'b) * ('b => bool)"
     1.5  
     1.6  consts
     1.7 -  start :: "('a, 'b)auto => 'b"
     1.8 -  next  :: "('a, 'b)auto => ('b => 'a => 'b)"
     1.9 -  fin   :: "('a, 'b)auto => ('b => bool)"
    1.10 -  nexts :: "('a, 'b)auto => 'b => 'a list => 'b"
    1.11 -  accepts :: "('a,'b) auto => 'a list => bool"  
    1.12 -  acc_prefix :: "('a, 'b)auto => 'b => 'a list => bool"
    1.13 +  start :: ('a, 'b)auto => 'b
    1.14 +  next  :: ('a, 'b)auto => ('b => 'a => 'b)
    1.15 +  fin   :: ('a, 'b)auto => ('b => bool)
    1.16 +  nexts :: ('a, 'b)auto => 'b => 'a list => 'b
    1.17 +  accepts :: ('a,'b) auto => 'a list => bool  
    1.18 +  acc_prefix :: ('a, 'b)auto => 'b => 'a list => bool
    1.19  
    1.20  defs
    1.21    start_def "start(A) == fst(A)"