inductive: no collective atts;

--- a/src/HOL/Induct/Mutil.thy	Fri Sep 28 20:08:28 2001 +0200
+++ b/src/HOL/Induct/Mutil.thy	Fri Sep 28 20:09:10 2001 +0200
@@ -17,15 +17,15 @@
 
 consts tiling :: "'a set set => 'a set set"
 inductive "tiling A"
-  intros [simp, intro]
-    empty: "{} \<in> tiling A"
-    Un: "a \<in> A ==> t \<in> tiling A ==> a \<inter> t = {} ==> a \<union> t \<in> tiling A"
+  intros
+    empty [simp, intro]: "{} \<in> tiling A"
+    Un [simp, intro]: "a \<in> A ==> t \<in> tiling A ==> a \<inter> t = {} ==> a \<union> t \<in> tiling A"
 
 consts domino :: "(nat \<times> nat) set set"
 inductive domino
-  intros [simp]
-    horiz: "{(i, j), (i, Suc j)} \<in> domino"
-    vertl: "{(i, j), (Suc i, j)} \<in> domino"
+  intros
+    horiz [simp]: "{(i, j), (i, Suc j)} \<in> domino"
+    vertl [simp]: "{(i, j), (Suc i, j)} \<in> domino"
 
 constdefs
   coloured :: "nat => (nat \<times> nat) set"

--- a/src/HOL/ex/BinEx.thy	Fri Sep 28 20:08:28 2001 +0200
+++ b/src/HOL/ex/BinEx.thy	Fri Sep 28 20:09:10 2001 +0200
@@ -240,12 +240,12 @@
 *}
 
 consts normal :: "bin set"
-inductive "normal"
-  intros [simp]
-    Pls: "Pls: normal"
-    Min: "Min: normal"
-    BIT_F: "w: normal ==> w \<noteq> Pls ==> w BIT False : normal"
-    BIT_T: "w: normal ==> w \<noteq> Min ==> w BIT True : normal"
+inductive normal
+  intros
+    Pls [simp]: "Pls: normal"
+    Min [simp]: "Min: normal"
+    BIT_F [simp]: "w: normal ==> w \<noteq> Pls ==> w BIT False : normal"
+    BIT_T [simp]: "w: normal ==> w \<noteq> Min ==> w BIT True : normal"
 
 text {*
   \medskip Binary arithmetic on normalized operands yields normalized