--- a/Nominal/Ex/Lambda.thy	Tue Apr 13 00:47:57 2010 +0200
+++ b/Nominal/Ex/Lambda.thy	Tue Apr 13 00:53:32 2010 +0200
@@ -141,6 +141,18 @@
 apply(tactic {* my_tac @{context} @{thms valid.intros} 1 *})
 done
 
+lemma
+  shows "valid Gamma \<longrightarrow> valid (p \<bullet> Gamma)"
+ML_prf {*
+val ({names, ...}, {raw_induct, intrs, elims, ...}) =
+      Inductive.the_inductive @{context} (Sign.intern_const @{theory} "valid")
+*}
+apply(tactic {* rtac raw_induct 1 *})
+apply(tactic {* my_tac @{context} @{thms valid.intros} 1 *})
+apply(tactic {* my_tac @{context} @{thms valid.intros} 1 *})
+done
+
+
 thm eqvts
 thm eqvts_raw
 
@@ -151,8 +163,20 @@
   | t_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : T1 \<rightarrow> T2 \<and> \<Gamma> \<turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : T2"
   | t_Lam[intro]: "\<lbrakk>atom x \<sharp> \<Gamma>; (x, T1) # \<Gamma> \<turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam x t : T1 \<rightarrow> T2"
 
-thm typing.induct
-ML {* Inductive.get_monos @{context} *}
+
+ML {* Inductive.the_inductive @{context} (Sign.intern_const @{theory} "typing") *}
+
+lemma 
+  shows "Gamma \<turnstile> t : T \<longrightarrow> (p \<bullet> Gamma) \<turnstile> (p \<bullet> t) : (p \<bullet> T)"
+ML_prf {*
+val ({names, ...}, {raw_induct, intrs, elims, ...}) =
+      Inductive.the_inductive @{context} (Sign.intern_const @{theory} "typing")
+*}
+apply(tactic {* rtac raw_induct 1 *})
+apply(tactic {* my_tac @{context} @{thms typing.intros} 1 *})
+apply(perm_strict_simp)
+apply(rule typing.intros)
+oops
 
 lemma uu[eqvt]:
   assumes a: "Gamma \<turnstile> t : T" 
@@ -168,10 +192,13 @@
 apply(rule impI)
 prefer 2
 apply(rule impI)
-apply(tactic {* my_tac @{context} @{thms typing.intros} 1 *})
+apply(simp)
+apply(auto)[1]
+apply(simp)
 apply(tactic {* my_tac @{context} @{thms typing.intros} 1 *})
 done
 
+(*
 inductive
   typing :: "(name\<times>ty) list \<Rightarrow> lam \<Rightarrow> ty \<Rightarrow> bool" ("_ \<turnstile> _ : _" [60,60,60] 60) 
 where
@@ -188,6 +215,37 @@
 apply(tactic {* my_tac @{context} @{thms typing.intros} 1 *})
 apply(tactic {* my_tac @{context} @{thms typing.intros} 1 *})
 done
+*)
+
+ML {*
+val inductive_atomize = @{thms induct_atomize};
+
+val atomize_conv =
+  MetaSimplifier.rewrite_cterm (true, false, false) (K (K NONE))
+    (HOL_basic_ss addsimps inductive_atomize);
+val atomize_intr = Conv.fconv_rule (Conv.prems_conv ~1 atomize_conv);
+fun atomize_induct ctxt = Conv.fconv_rule (Conv.prems_conv ~1
+  (Conv.params_conv ~1 (K (Conv.prems_conv ~1 atomize_conv)) ctxt));
+*}
+
+ML {*
+val ({names, ...}, {raw_induct, intrs, elims, ...}) =
+      Inductive.the_inductive @{context} (Sign.intern_const @{theory} "typing")
+*}
+
+ML {* val ind_params = Inductive.params_of raw_induct *}
+ML {* val raw_induct = atomize_induct @{context} raw_induct; *}
+ML {* val elims = map (atomize_induct @{context}) elims; *}
+ML {* val monos = Inductive.get_monos @{context}; *}
+
+lemma 
+  shows "Gamma \<turnstile> t : T \<longrightarrow> (p \<bullet> Gamma) \<turnstile> (p \<bullet> t) : (p \<bullet> T)"
+apply(tactic {* rtac raw_induct 1 *})
+apply(tactic {* my_tac @{context} intrs 1 *})
+apply(perm_strict_simp)
+apply(rule typing.intros)
+oops
+
 
 thm eqvts
 thm eqvts_raw

--- a/Nominal/FSet.thy	Tue Apr 13 00:47:57 2010 +0200
+++ b/Nominal/FSet.thy	Tue Apr 13 00:53:32 2010 +0200
@@ -43,8 +43,7 @@
 quotient_definition
   fin ("_ |\<in>| _" [50, 51] 50)
 where
-  "fin :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool"
-is "memb"
+  "fin :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" is "memb"
 
 abbreviation
   fnotin :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ |\<notin>| _" [50, 51] 50)
@@ -63,7 +62,7 @@
   shows "(op = ===> op \<approx> ===> op \<approx>) op # op #"
 by simp
 
-section {* Augmenting a set -- @{const finsert} *}
+section {* Augmenting an fset -- @{const finsert} *}
 
 lemma nil_not_cons:
   shows