| changeset 8732 | aef229ca5e77 |
| parent 8703 | 816d8f6513be |
| child 14428 | bb2b0e10d9be |
--- a/src/HOL/Lex/AutoChopper1.thy Mon Apr 17 14:27:10 2000 +0200 +++ b/src/HOL/Lex/AutoChopper1.thy Tue Apr 18 00:36:02 2000 +0200 @@ -17,7 +17,7 @@ No proofs yet. *) -AutoChopper1 = DA + Chopper + Main + +AutoChopper1 = DA + Chopper + consts acc :: "(('a,'s)da * 'a list * 's * 'a list list * 'a list * 'a list)