inductive2: canonical specification syntax;

--- a/src/HOL/FunDef.thy	Tue Nov 14 17:55:30 2006 +0100
+++ b/src/HOL/FunDef.thy	Tue Nov 14 22:16:54 2006 +0100
@@ -48,8 +48,8 @@
 
 inductive2 accP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
   for r :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
-intros
-    accPI: "(!!y. r y x ==> accP r y) ==> accP r x"
+where
+  accPI: "(!!y. r y x ==> accP r y) ==> accP r x"
 
 
 theorem accP_induct:

--- a/src/HOL/Nominal/Examples/Weakening.thy	Tue Nov 14 17:55:30 2006 +0100
+++ b/src/HOL/Nominal/Examples/Weakening.thy	Tue Nov 14 22:16:54 2006 +0100
@@ -28,9 +28,9 @@
 text {* valid contexts *}
 inductive2
   valid :: "(name\<times>ty) list \<Rightarrow> bool"
-intros
-v1[intro]: "valid []"
-v2[intro]: "\<lbrakk>valid \<Gamma>;a\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> valid ((a,\<sigma>)#\<Gamma>)"
+where
+    v1[intro]: "valid []"
+  | v2[intro]: "\<lbrakk>valid \<Gamma>;a\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> valid ((a,\<sigma>)#\<Gamma>)"
 
 lemma eqvt_valid:
   fixes   pi:: "name prm"
@@ -43,10 +43,10 @@
 text{* typing judgements *}
 inductive2
   typing :: "(name\<times>ty) list\<Rightarrow>lam\<Rightarrow>ty\<Rightarrow>bool" (" _ \<turnstile> _ : _ " [80,80,80] 80) 
-intros
-t_Var[intro]: "\<lbrakk>valid \<Gamma>; (a,\<tau>)\<in>set \<Gamma>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> Var a : \<tau>"
-t_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : \<tau>\<rightarrow>\<sigma>; \<Gamma> \<turnstile> t2 : \<tau>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : \<sigma>"
-t_Lam[intro]: "\<lbrakk>a\<sharp>\<Gamma>;((a,\<tau>)#\<Gamma>) \<turnstile> t : \<sigma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [a].t : \<tau>\<rightarrow>\<sigma>"
+where
+    t_Var[intro]: "\<lbrakk>valid \<Gamma>; (a,\<tau>)\<in>set \<Gamma>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> Var a : \<tau>"
+  | t_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : \<tau>\<rightarrow>\<sigma>; \<Gamma> \<turnstile> t2 : \<tau>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : \<sigma>"
+  | t_Lam[intro]: "\<lbrakk>a\<sharp>\<Gamma>;((a,\<tau>)#\<Gamma>) \<turnstile> t : \<sigma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [a].t : \<tau>\<rightarrow>\<sigma>"
 
 lemma eqvt_typing: 
   fixes pi:: "name prm"