equal
deleted
inserted
replaced
17 |
17 |
18 But both versions are far too specific. Better development in Scanner.thy and |
18 But both versions are far too specific. Better development in Scanner.thy and |
19 its antecedents. |
19 its antecedents. |
20 *) |
20 *) |
21 |
21 |
22 AutoChopper = Prefix + DA + Chopper + |
22 AutoChopper = DA + Chopper + |
23 |
23 |
24 constdefs |
24 constdefs |
25 is_auto_chopper :: (('a,'s)da => 'a chopper) => bool |
25 is_auto_chopper :: (('a,'s)da => 'a chopper) => bool |
26 "is_auto_chopper(chopperf) == |
26 "is_auto_chopper(chopperf) == |
27 !A. is_longest_prefix_chopper(accepts A)(chopperf A)" |
27 !A. is_longest_prefix_chopper(accepts A)(chopperf A)" |