src/HOL/Isar_examples/MultisetOrder.thy

 lemma less_add: "(N, M0 + {#a#}) : mult1 r ==>
     (EX M. (M, M0) : mult1 r & N = M + {#a#}) |
     (EX K. (ALL b. elem K b --> (b, a) : r) & N = M0 + K)"
   (concl is "?case1 (mult1 r) | ?case2");
 proof (unfold mult1_def);
-  let ?r = "\<lambda>K a. ALL b. elem K b --> (b, a) : r";
-  let ?R = "\<lambda>N M. EX a M0 K. M = M0 + {#a#} & N = M0 + K & ?r K a";
+  let ?r = "\\<lambda>K a. ALL b. elem K b --> (b, a) : r";
+  let ?R = "\\<lambda>N M. EX a M0 K. M = M0 + {#a#} & N = M0 + K & ?r K a";
   let ?case1 = "?case1 {(N, M). ?R N M}";
 
   assume "(N, M0 + {#a#}) : {(N, M). ?R N M}";
   hence "EX a' M0' K.
       M0 + {#a#} = M0' + {#a'#} & N = M0' + K & ?r K a'"; by simp;

       next;
 	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 (induct K rule: multiset_induct);
+	proof (induct K in rule: multiset_induct);
 	  from M0; have "M0 + {#} : ?W"; by simp;
 	  thus "?P {#}"; ..;
 
 	  fix K x; assume hyp: "?P K";
 	  show "?P (K + {#x#})";

   }}; note tedious_reasoning = this;
 
   assume wf: "wf r";
   fix M;
   show "M : ?W";
-  proof (induct M rule: multiset_induct);
+  proof (induct M in rule: multiset_induct);
     show "{#} : ?W";
     proof (rule accI);
       fix b; assume "(b, {#}) : ?R";
       with not_less_empty; show "b : ?W"; by contradiction;
     qed;