# HG changeset patch
# User wenzelm
# Date 936872744 -7200
# Node ID 505f6f8e9dcf2e3bf0c640c9d66a0320021425d1
# Parent  fa534e4f7e49d659642afe9aae3b2f3e359d3290
tuned;

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#}) |