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.7 - \footnote{Original tactic script by Tobias Nipkow (see also
     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"