--- a/src/HOL/Lex/MaxChop.ML Fri Jul 03 10:36:47 1998 +0200
+++ b/src/HOL/Lex/MaxChop.ML Fri Jul 03 10:37:04 1998 +0200
@@ -17,7 +17,7 @@
val chopr_rule = let val [chopr_rule] = chopr.rules in lemma RS chopr_rule end;
-Goalw [chop_def] "!!splitf. reducing splitf ==> \
+Goalw [chop_def] "reducing splitf ==> \
\ chop splitf xs = (let (pre,post) = splitf xs \
\ in if pre=[] then ([],xs) \
\ else let (xss,zs) = chop splitf post \
@@ -27,11 +27,11 @@
qed "chop_rule";
Goalw [is_maxsplitter_def,reducing_def]
- "!!splitf. is_maxsplitter P splitf ==> reducing splitf";
+ "is_maxsplitter P splitf ==> reducing splitf";
by(Asm_full_simp_tac 1);
qed "is_maxsplitter_reducing";
-Goal "!!P. is_maxsplitter P splitf ==> \
+Goal "is_maxsplitter P splitf ==> \
\ !yss zs. chop splitf xs = (yss,zs) --> xs = concat yss @ zs";
by(res_inst_tac [("xs","xs")] length_induct 1);
by(asm_simp_tac (simpset() delsplits [split_if]
@@ -41,7 +41,7 @@
addsplits [split_split]) 1);
qed_spec_mp "chop_concat";
-Goal "!!P. is_maxsplitter P splitf ==> \
+Goal "is_maxsplitter P splitf ==> \
\ !yss zs. chop splitf xs = (yss,zs) --> (!ys : set yss. ys ~= [])";
by(res_inst_tac [("xs","xs")] length_induct 1);
by(asm_simp_tac (simpset() addsimps [chop_rule,is_maxsplitter_reducing]