diff -r 8f5f7abe22c1 -r 632b08744613 Nominal/Test.thy
--- a/Nominal/Test.thy	Thu Mar 11 12:30:53 2010 +0100
+++ b/Nominal/Test.thy	Thu Mar 11 13:34:45 2010 +0100
@@ -15,21 +15,18 @@
 where
   "bi (BP x t) = {atom x}"
 
+thm lam_bp_fv
+thm lam_bp_inject
+thm lam_bp_bn
+thm lam_bp_perm
+thm lam_bp_induct
+thm lam_bp_distinct
+
 (* compat should be
 compat (BP x t) pi (BP x' t')
   \<equiv> alpha_trm t t' \<and> pi o x = x'
 *)
 
-typ lam_raw
-term VAR_raw
-term APP_raw
-term LET_raw
-term Test.BP_raw
-thm bi_raw.simps
-thm permute_lam_raw_permute_bp_raw.simps
-thm alpha_lam_raw_alpha_bp_raw_alpha_bi_raw.intros[no_vars]
-(*thm fv_lam_raw_fv_bp_raw.simps[no_vars]*)
-
 text {* example 2 *}
 
 nominal_datatype trm' =
@@ -48,6 +45,12 @@
 | "f (PD x y) = {atom x, atom y}"
 | "f (PS x) = {atom x}"
 
+thm trm'_pat'_fv
+thm trm'_pat'_inject
+thm trm'_pat'_bn
+thm trm'_pat'_perm
+thm trm'_pat'_induct
+thm trm'_pat'_distinct
 
 (* compat should be
 compat (PN) pi (PN) == True
@@ -55,16 +58,6 @@
 compat (PD p1 p2) pi (PD p1' p2') == compat p1 pi p1' & compat p2 pi p2'
 *)
 
-
-thm alpha_trm'_raw_alpha_pat'_raw_alpha_f_raw.intros[no_vars]
-(*thm fv_trm'_raw_fv_pat'_raw.simps[no_vars]*)
-thm f_raw.simps
-(*thm trm'_pat'_induct
-thm trm'_pat'_perm
-thm trm'_pat'_fv
-thm trm'_pat'_bn
-thm trm'_pat'_inject*)
-
 nominal_datatype trm0 =
   Var0 "name"
 | App0 "trm0" "trm0"
@@ -81,11 +74,12 @@
 | "f0 (PS0 x) = {atom x}"
 | "f0 (PD0 p1 p2) = (f0 p1) \<union> (f0 p2)"
 
-thm f0_raw.simps
-(*thm trm0_pat0_induct
+thm trm0_pat0_fv
+thm trm0_pat0_inject
+thm trm0_pat0_bn
 thm trm0_pat0_perm
-thm trm0_pat0_fv
-thm trm0_pat0_bn*)
+thm trm0_pat0_induct
+thm trm0_pat0_distinct
 
 text {* example type schemes *}
 
@@ -95,6 +89,13 @@
 and  tyS =
   All xs::"name set" ty::"t" bind xs in ty
 
+thm t_tyS_fv
+thm t_tyS_inject
+thm t_tyS_bn
+thm t_tyS_perm
+thm t_tyS_induct
+thm t_tyS_distinct
+
 (* example 1 from Terms.thy *)
 
 nominal_datatype trm1 =
@@ -113,8 +114,12 @@
 | "bv1 (BP1 bp1 bp2) = (bv1 bp1) \<union> (bv1 bp2)"
 | "bv1 (BV1 x) = {atom x}"
 
-
-thm bv1_raw.simps
+thm trm1_bp1_fv
+thm trm1_bp1_inject
+thm trm1_bp1_bn
+thm trm1_bp1_perm
+thm trm1_bp1_induct
+thm trm1_bp1_distinct
 
 text {* example 3 from Terms.thy *}
 
@@ -132,6 +137,12 @@
   "bv3 ANil = {}"
 | "bv3 (ACons x t as) = {atom x} \<union> (bv3 as)"
 
+thm trm3_rassigns3_fv
+thm trm3_rassigns3_inject
+thm trm3_rassigns3_bn
+thm trm3_rassigns3_perm
+thm trm3_rassigns3_induct
+thm trm3_rassigns3_distinct
 
 (* compat should be
 compat (ANil) pi (PNil) \<equiv> TRue
@@ -153,6 +164,13 @@
   "bv5 Lnil = {}"
 | "bv5 (Lcons n t ltl) = {atom n} \<union> (bv5 ltl)"
 
+thm trm5_lts_fv
+thm trm5_lts_inject
+thm trm5_lts_bn
+thm trm5_lts_perm
+thm trm5_lts_induct
+thm trm5_lts_distinct
+
 (* example from my PHD *)
 
 atom_decl coname
@@ -166,9 +184,12 @@
 |  ImpL c::"coname" t1::"phd" n::"name" t2::"phd" "name"        bind c in t1, bind n in t2
 |  ImpR c::"coname" n::"name" t::"phd" "coname"                 bind n in t, bind c in t
 
-thm alpha_phd_raw.intros[no_vars]
-thm fv_phd_raw.simps[no_vars]
-
+thm phd_fv
+thm phd_inject
+thm phd_bn
+thm phd_perm
+thm phd_induct
+thm phd_distinct
 
 (* example form Leroy 96 about modules; OTT *)
 
@@ -223,8 +244,15 @@
 | "Cbinders (SStru x S) = {atom x}"
 | "Cbinders (SVal v T) = {atom v}"
 
+thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_fv
+thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_inject
+thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_bn
+thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_perm
+thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_induct
+thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_distinct
 
 (* example 3 from Peter Sewell's bestiary *)
+
 nominal_datatype exp =
   VarP "name"
 | AppP "exp" "exp"
@@ -240,7 +268,13 @@
   "bp' (PVar x) = {atom x}"
 | "bp' (PUnit) = {}"
 | "bp' (PPair p1 p2) = bp' p1 \<union> bp' p2"
-thm alpha_exp_raw_alpha_pat3_raw_alpha_bp'_raw.intros
+
+thm exp_pat3_fv
+thm exp_pat3_inject
+thm exp_pat3_bn
+thm exp_pat3_perm
+thm exp_pat3_induct
+thm exp_pat3_distinct
 
 (* example 6 from Peter Sewell's bestiary *)
 nominal_datatype exp6 =
@@ -257,7 +291,13 @@
   "bp6 (PVar' x) = {atom x}"
 | "bp6 (PUnit') = {}"
 | "bp6 (PPair' p1 p2) = bp6 p1 \<union> bp6 p2"
-thm alpha_exp6_raw_alpha_pat6_raw_alpha_bp6_raw.intros
+
+thm exp6_pat6_fv
+thm exp6_pat6_inject
+thm exp6_pat6_bn
+thm exp6_pat6_perm
+thm exp6_pat6_induct
+thm exp6_pat6_distinct
 
 (* THE REST ARE NOT SUPPOSED TO WORK YET *)