--- a/src/HOL/Isar_examples/MultisetOrder.thy Fri Sep 03 14:21:59 1999 +0200
+++ b/src/HOL/Isar_examples/MultisetOrder.thy Fri Sep 03 14:22:12 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 a K")
+ fix K; assume "ALL b. elem K b --> (b, a) : r" (is "??A K")
and N: "N = M0 + K";
- have "??A a K --> M0 + K : ??W" (is "??P K");
+ have "??A K --> 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 a (K + {#x#})";
+ assume a: "??A (K + {#x#})";
hence "(x, a) : r"; by simp;
with wf_hyp [RS spec]; have b: "ALL M:??W. M + {#x#} : ??W"; ..;