| changeset 4910 | 697d17fe1665 |
| parent 4832 | bc11b5b06f87 |
| child 5069 | 3ea049f7979d |
--- a/src/HOL/Lex/MaxChop.ML Mon May 11 13:18:25 1998 +0200 +++ b/src/HOL/Lex/MaxChop.ML Mon May 11 14:40:40 1998 +0200 @@ -6,7 +6,7 @@ (* Termination of chop *) -goalw thy [reducing_def] "reducing(%qs. maxsplit P [] qs ([],qs))"; +goalw thy [reducing_def] "reducing(%qs. maxsplit P ([],qs) [] qs)"; by(asm_full_simp_tac (simpset() addsimps [maxsplit_eq]) 1); qed "reducing_maxsplit";