# HG changeset patch
# User wenzelm
# Date 970605319 -7200
# Node ID fe2a4e018dbf1ab9c5a35829190f1306e97a884d
# Parent  86c39bba873f4d605f3ec0e8f53fe0033baa7001
hide declaratations;

diff -r 86c39bba873f -r fe2a4e018dbf src/HOL/Isar_examples/MultisetOrder.thy
--- a/src/HOL/Isar_examples/MultisetOrder.thy	Tue Oct 03 22:34:49 2000 +0200
+++ b/src/HOL/Isar_examples/MultisetOrder.thy	Tue Oct 03 22:35:19 2000 +0200
@@ -14,12 +14,10 @@
  \url{http://isabelle.in.tum.de/library/HOL/Induct/Multiset.html}),
  based on a pen-and-paper proof due to Wilfried Buchholz.}\isanewline
 *}
-
-(* FIXME move? *)
-theorems [induct type: multiset] = multiset_induct
-theorems [induct set: wf] = wf_induct
-theorems [induct set: acc] = acc_induct
-
+(*<*)(* FIXME move? *)
+declare multiset_induct [induct type: multiset]
+declare wf_induct [induct set: wf]
+declare acc_induct [induct set: acc](*>*)
 
 subsection {* A technical lemma *}