# HG changeset patch
# User bulwahn
# Date 1266929871 -3600
# Node ID 4123977b469d1e95bb7b5c986384f58211c39471
# Parent  c9f428269b3826dd470e22dd8ec2f00dbe92807a
adding ROOT.ML to HOL-Mutabelle session; uncommenting HOL.induct constants in Mutabelle session

diff -r c9f428269b38 -r 4123977b469d src/HOL/Mutabelle/ROOT.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Mutabelle/ROOT.ML	Tue Feb 23 13:57:51 2010 +0100
@@ -0,0 +1,3 @@
+
+use_thy "MutabelleExtra";
+
diff -r c9f428269b38 -r 4123977b469d src/HOL/Mutabelle/mutabelle_extra.ML
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Tue Feb 23 13:36:15 2010 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Tue Feb 23 13:57:51 2010 +0100
@@ -192,9 +192,9 @@
 
 val forbidden =
  [(* (@{const_name "power"}, "'a"), *)
-  (@{const_name HOL.induct_equal}, "'a"),
-  (@{const_name HOL.induct_implies}, "'a"),
-  (@{const_name HOL.induct_conj}, "'a"),
+  (*(@{const_name induct_equal}, "'a"),
+  (@{const_name induct_implies}, "'a"),
+  (@{const_name induct_conj}, "'a"),*)
   (@{const_name "undefined"}, "'a"),
   (@{const_name "default"}, "'a"),
   (@{const_name "dummy_pattern"}, "'a::{}") (*,