--- a/src/HOL/Lex/AutoMaxChop.ML Mon Jun 22 17:13:09 1998 +0200
+++ b/src/HOL/Lex/AutoMaxChop.ML Mon Jun 22 17:26:46 1998 +0200
@@ -4,11 +4,11 @@
Copyright 1998 TUM
*)
-goal thy "delta A (xs@[y]) q = next A y (delta A xs q)";
+Goal "delta A (xs@[y]) q = next A y (delta A xs q)";
by(Simp_tac 1);
qed "delta_snoc";
-goal thy
+Goal
"!q ps res. auto_split A (delta A ps q) res ps xs = \
\ maxsplit (%ys. fin A (delta A ys q)) res ps xs";
by(induct_tac "xs" 1);
@@ -17,20 +17,20 @@
delsimps [delta_append]) 1);
qed_spec_mp "auto_split_lemma";
-goalw thy [accepts_def]
+Goalw [accepts_def]
"auto_split A (start A) res [] xs = maxsplit (accepts A) res [] xs";
by(stac ((read_instantiate [("s","start A")] delta_Nil) RS sym) 1);
by(stac auto_split_lemma 1);
by(Simp_tac 1);
qed_spec_mp "auto_split_is_maxsplit";
-goal thy
+Goal
"is_maxsplitter (accepts A) (%xs. auto_split A (start A) ([],xs) [] xs)";
by(simp_tac (simpset() addsimps
[auto_split_is_maxsplit,is_maxsplitter_maxsplit]) 1);
qed "is_maxsplitter_auto_split";
-goalw thy [auto_chop_def]
+Goalw [auto_chop_def]
"is_maxchopper (accepts A) (auto_chop A)";
br is_maxchopper_chop 1;
br is_maxsplitter_auto_split 1;