summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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;