src/HOL/Isar_examples/MultisetOrder.thy
changeset 7565 bfa85f429629
parent 7530 505f6f8e9dcf
child 7761 7fab9592384f
     1.1 --- a/src/HOL/Isar_examples/MultisetOrder.thy	Tue Sep 21 17:30:11 1999 +0200
     1.2 +++ b/src/HOL/Isar_examples/MultisetOrder.thy	Tue Sep 21 17:30:55 1999 +0200
     1.3 @@ -40,7 +40,7 @@
     1.4        with N; have n: "N = K' + K + {#a#}"; by (simp add: union_ac);
     1.5  
     1.6        assume "M0 = K' + {#a'#}";
     1.7 -      with r; have "?R (K' + K) M0"; by simp blast;
     1.8 +      with r; have "?R (K' + K) M0"; by blast;
     1.9        with n; have ?case1; by simp; thus ?thesis; ..;
    1.10      qed;
    1.11    qed;