| changeset 7530 | 505f6f8e9dcf |
| parent 7527 | 9e2dddd8b81f |
| child 7565 | bfa85f429629 |
--- a/src/HOL/Isar_examples/MultisetOrder.thy Thu Sep 09 12:25:30 1999 +0200 +++ b/src/HOL/Isar_examples/MultisetOrder.thy Thu Sep 09 12:25:44 1999 +0200 @@ -11,9 +11,6 @@ theory MultisetOrder = Multiset:; -(* FIXME *) -theorems [intro!!] = disjI1 disjI2; - lemma less_add: "(N, M0 + {#a#}) : mult1 r ==> (EX M. (M, M0) : mult1 r & N = M + {#a#}) |