src/HOL/Isar_examples/MultisetOrder.thy
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#}) |