--- a/src/HOL/Nominal/Examples/Weakening.thy Wed Jul 11 11:35:17 2007 +0200
+++ b/src/HOL/Nominal/Examples/Weakening.thy Wed Jul 11 11:36:06 2007 +0200
@@ -27,7 +27,7 @@
text {* valid contexts *}
-inductive2
+inductive
valid :: "(name\<times>ty) list \<Rightarrow> bool"
where
v1[intro]: "valid []"
@@ -36,7 +36,7 @@
equivariance valid
text{* typing judgements *}
-inductive2
+inductive
typing :: "(name\<times>ty) list\<Rightarrow>lam\<Rightarrow>ty\<Rightarrow>bool" ("_ \<turnstile> _ : _" [60,60,60] 60)
where
t_Var[intro]: "\<lbrakk>valid \<Gamma>; (x,T)\<in>set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var x : T"