--- a/Nominal/Ex/Lambda.thy	Tue May 24 19:39:38 2011 +0200
+++ b/Nominal/Ex/Lambda.thy	Wed May 25 21:38:50 2011 +0200
@@ -10,15 +10,17 @@
 | eVar nat
 
 inductive 
-  eval :: "expr \<Rightarrow> nat \<Rightarrow> bool"
+  eval :: "expr \<Rightarrow> nat list \<Rightarrow> bool"
 where
-  evCnst: "eval (eCnst c) 0"
-| evVar: "eval (eVar n) 2"
+  evCnst1: "eval (eCnst c) [2,1]"
+| evCnst2: "eval (eCnst b) [1,2]"
+| evVar: "eval (eVar n) [1]"
 
 inductive_cases 
-  evInv_Cnst: "eval (eCnst c) m"
+  evInv_Cnst: "eval (eCnst c) [1,2]"
 
-thm evInv_Cnst[simplified expr.distinct expr.eq_iff]
+thm evInv_Cnst
+
 
 
 atom_decl name
@@ -143,7 +145,8 @@
 defer
 apply(rule_tac y="x" in lam.exhaust)
 apply(simp_all)[3]
-apply(simp_all add: lam.distinct lam.eq_iff)
+apply(auto)[1]
+apply(simp_all)
 apply (erule Abs1_eq_fdest)
 apply(simp add: supp_removeAll fresh_def)
 apply(drule supp_eqvt_at)

--- a/Nominal/Ex/Multi_Recs2.thy	Tue May 24 19:39:38 2011 +0200
+++ b/Nominal/Ex/Multi_Recs2.thy	Wed May 25 21:38:50 2011 +0200
@@ -83,9 +83,6 @@
 thm fun_recs.fsupp
 thm fun_recs.supp
 
-
-
-
 lemma
   fixes c::"'a::fs"
   assumes "\<And>name c. P1 c (Var name)"
@@ -106,16 +103,21 @@
   apply(raw_tactic {* Induction_Schema.induction_schema_tac @{context} @{thms assms} *})
   apply(rule_tac y="exp" and c="c" in fun_recs.strong_exhaust(1))
   apply(simp_all)[4]
+  apply(blast)
   apply(rule_tac ya="fnclause" and c="c" in fun_recs.strong_exhaust(2))
-  apply(simp_all)[1]
+  apply(blast)
   apply(rule_tac yb="fnclauses" in fun_recs.strong_exhaust(3))
-  apply(simp_all)[2]
+  apply(blast)
+  apply(blast)
   apply(rule_tac yc="lrb" in fun_recs.strong_exhaust(4))
-  apply(simp_all)[1]
+  apply(blast)
   apply(rule_tac yd="lrbs" in fun_recs.strong_exhaust(5))
-  apply(simp_all)[2]
+  apply(blast)
+  apply(blast)
   apply(rule_tac ye="pat" in fun_recs.strong_exhaust(6))
-  apply(simp_all)[3]
+  apply(blast)
+  apply(blast)
+  apply(blast)
   apply(tactic {* prove_termination_ind @{context} 1 *})
   apply(simp_all add: fun_recs.size)
   done

--- a/Nominal/Ex/TypeSchemes.thy	Tue May 24 19:39:38 2011 +0200
+++ b/Nominal/Ex/TypeSchemes.thy	Wed May 25 21:38:50 2011 +0200
@@ -184,15 +184,14 @@
 apply (case_tac x)
 apply simp apply clarify 
 apply (rule_tac y="b" in ty_tys.exhaust(1))
-apply (auto simp add: ty_tys.eq_iff)[1]
-apply (auto simp add: ty_tys.eq_iff)[1]
-apply blast
+apply (auto)[1]
+apply (auto)[1]
 apply simp apply clarify 
 apply (rule_tac ya="b" and c="a" in ty_tys.strong_exhaust(2))
-apply (auto simp add: ty_tys.eq_iff)[1]
-apply (auto simp add: ty_tys.distinct)
-apply (auto simp add: ty_tys.eq_iff ty_tys.distinct)[2]
+apply (auto)[1]
+apply (auto)[5]
 --"LAST GOAL"
+apply(simp del: ty_tys.eq_iff)
 thm meta_eq_to_obj_eq[OF subst_def, symmetric, unfolded fun_eq_iff]
 apply (simp add: meta_eq_to_obj_eq[OF subst_def, symmetric, unfolded fun_eq_iff])
 apply (subgoal_tac "eqvt_at (\<lambda>(l, r). subst l r) (\<theta>', T)")
@@ -230,7 +229,6 @@
 apply clarify
 --"This is exactly the assumption for the properly defined function"
 defer
-apply (simp add: ty_tys.eq_iff)
 apply (simp only: Abs_eq_res_set)
 apply (subgoal_tac "(atom ` fset xsa \<inter> supp Ta - atom ` fset xs \<inter> supp T) \<sharp>* ([atom ` fset xs \<inter> supp (subst \<theta>' T)]set. T)")
 apply (subst (asm) Abs_eq_iff2)
@@ -361,8 +359,6 @@
 apply(blast)
 apply(blast)
 apply(simp_all add: ty2.distinct)
-apply(simp add: ty2.eq_iff)
-apply(simp add: ty2.eq_iff)
 apply(subgoal_tac "\<And>p x r. subst_graph x r \<Longrightarrow> subst_graph (p \<bullet> x) (p \<bullet> r)")
 apply(simp add: eqvt_def)
 apply(rule allI)

--- a/Nominal/Nominal2.thy	Tue May 24 19:39:38 2011 +0200
+++ b/Nominal/Nominal2.thy	Wed May 25 21:38:50 2011 +0200
@@ -43,6 +43,7 @@
 val eqvt_attr = Attrib.internal (K Nominal_ThmDecls.eqvt_add)
 val rsp_attr = Attrib.internal (K Quotient_Info.rsp_rules_add)
 val simp_attr = Attrib.internal (K Simplifier.simp_add)
+val induct_attr = Attrib.internal (K Induct.induct_simp_add)
 *}
 
 section{* Interface for nominal_datatype *}
@@ -455,8 +456,8 @@
   val case_names_attr = Attrib.internal (K (Rule_Cases.case_names cnstr_names))
 
   val (_, lthy9') = lthyC
-     |> Local_Theory.note ((thms_suffix "distinct", []), qdistincts) 
-     ||>> Local_Theory.note ((thms_suffix "eq_iff", []), qeq_iffs')
+     |> Local_Theory.note ((thms_suffix "distinct", [induct_attr, simp_attr]), qdistincts) 
+     ||>> Local_Theory.note ((thms_suffix "eq_iff", [induct_attr, simp_attr]), qeq_iffs')
      ||>> Local_Theory.note ((thms_suffix "fv_defs", []), qfv_defs) 
      ||>> Local_Theory.note ((thms_suffix "bn_defs", []), qbn_defs) 
      ||>> Local_Theory.note ((thms_suffix "perm_simps", [eqvt_attr, simp_attr]), qperm_simps)