diff -r fa534e4f7e49 -r 505f6f8e9dcf src/HOL/Isar_examples/MultisetOrder.thy
--- 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#}) |