Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned;
authorwenzelm
Thu, 09 Sep 1999 12:25:44 +0200
changeset 7530 505f6f8e9dcf
parent 7529 fa534e4f7e49
child 7531 99c7e60d6b3f
tuned;
src/HOL/Isar_examples/MultisetOrder.thy file | annotate | diff | comparison | revisions 
--- 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#}) |
isabelle