# HG changeset patch
# User wenzelm
# Date 936363121 -7200
# Node ID d643b3c4996aa8afa2427533c96195fa11f8fddb
# Parent  e329ca03fd005b05b83ac18fff85eff95055b44a
tuned;

diff -r e329ca03fd00 -r d643b3c4996a src/HOL/Isar_examples/MultisetOrder.thy
--- a/src/HOL/Isar_examples/MultisetOrder.thy	Fri Sep 03 14:23:15 1999 +0200
+++ b/src/HOL/Isar_examples/MultisetOrder.thy	Fri Sep 03 14:52:01 1999 +0200
@@ -36,10 +36,10 @@
 	hence "M + {#a#} : ??W"; ..;
 	thus "N : ??W"; by (simp only: N);
       next;
-	fix K; assume "ALL b. elem K b --> (b, a) : r" (is "??A K")
-	  and N: "N = M0 + K";
-
-	have "??A K --> M0 + K : ??W" (is "??P K");
+	fix K;
+	assume N: "N = M0 + K";
+	assume "ALL b. elem K b --> (b, a) : r";
+	have "??this --> M0 + K : ??W" (is "??P K");
 	proof (rule multiset_induct [of _ K]);
 	  from M0; have "M0 + {#} : ??W"; by simp;
 	  thus "??P {#}"; ..;
@@ -47,7 +47,7 @@
 	  fix K x; assume hyp: "??P K";
 	  show "??P (K + {#x#})";
 	  proof;
-	    assume a: "??A (K + {#x#})";
+	    assume a: "ALL b. elem (K + {#x#}) b --> (b, a) : r";
 	    hence "(x, a) : r"; by simp;
 	    with wf_hyp [RS spec]; have b: "ALL M:??W. M + {#x#} : ??W"; ..;