equal
deleted
inserted
replaced
15 Hope: acc is easier to verify than AutoChopper.acc because simpler. |
15 Hope: acc is easier to verify than AutoChopper.acc because simpler. |
16 |
16 |
17 No proofs yet. |
17 No proofs yet. |
18 *) |
18 *) |
19 |
19 |
20 AutoChopper1 = DA + Chopper + |
20 theory AutoChopper1 = DA + Chopper: |
21 |
21 |
22 consts |
22 consts |
23 acc :: "(('a,'s)da * 'a list * 's * 'a list list * 'a list * 'a list) |
23 acc :: "(('a,'s)da * 'a list * 's * 'a list list * 'a list * 'a list) |
24 => 'a list list * 'a list" |
24 => 'a list list * 'a list" |
25 recdef acc "inv_image (less_than <*lex*> less_than) |
25 recdef acc "inv_image (less_than <*lex*> less_than) |