src/HOL/Isar_examples/MultisetOrder.thy
 changeset 7982 d534b897ce39 parent 7968 964b65b4e433 child 8281 188e2924433e
```     1.1 --- a/src/HOL/Isar_examples/MultisetOrder.thy	Sat Oct 30 20:13:16 1999 +0200
1.2 +++ b/src/HOL/Isar_examples/MultisetOrder.thy	Sat Oct 30 20:20:48 1999 +0200
1.3 @@ -10,7 +10,7 @@
1.4  theory MultisetOrder = Multiset:;
1.5
1.6  text_raw {*
1.8 + \footnote{Original tactic script by Tobias Nipkow (see
1.9   \url{http://isabelle.in.tum.de/library/HOL/Induct/Multiset.html}),
1.10   based on a pen-and-paper proof due to Wilfried Buchholz.}
1.11  *};
1.12 @@ -22,8 +22,8 @@
1.13      (EX K. (ALL b. elem K b --> (b, a) : r) & N = M0 + K)"
1.14    (concl is "?case1 (mult1 r) | ?case2");
1.15  proof (unfold mult1_def);
1.16 -  let ?r = "%K a. ALL b. elem K b --> (b, a) : r";
1.17 -  let ?R = "%N M. EX a M0 K. M = M0 + {#a#} & N = M0 + K & ?r K a";
1.18 +  let ?r = "\<lambda>K a. ALL b. elem K b --> (b, a) : r";
1.19 +  let ?R = "\<lambda>N M. EX a M0 K. M = M0 + {#a#} & N = M0 + K & ?r K a";
1.20    let ?case1 = "?case1 {(N, M). ?R N M}";
1.21
1.22    assume "(N, M0 + {#a#}) : {(N, M). ?R N M}";
1.23 @@ -61,7 +61,6 @@
1.24  proof;
1.25    let ?R = "mult1 r";
1.26    let ?W = "acc ?R";
1.27 -
1.28    {{;
1.29      fix M M0 a;
1.30      assume M0: "M0 : ?W"
```