fixed the examples for the new eqvt-procedure....temporarily disabled Manual/Term4.thy
--- a/Nominal/Ex/Classical.thy Wed May 12 16:33:50 2010 +0100
+++ b/Nominal/Ex/Classical.thy Wed May 12 16:59:53 2010 +0100
@@ -67,7 +67,7 @@
thm alpha.intros
equivariance alpha
-equivariance alpha_trm_raw
+
thm eqvts_raw
--- a/Nominal/Ex/CoreHaskell.thy Wed May 12 16:33:50 2010 +0100
+++ b/Nominal/Ex/CoreHaskell.thy Wed May 12 16:59:53 2010 +0100
@@ -652,10 +652,6 @@
thm eqvts
thm eqvts_raw
-equivariance alpha_tkind_raw
-
-thm eqvts
-thm eqvts_raw
end
--- a/Nominal/Ex/Ex1rec.thy Wed May 12 16:33:50 2010 +0100
+++ b/Nominal/Ex/Ex1rec.thy Wed May 12 16:59:53 2010 +0100
@@ -30,7 +30,6 @@
ML {* Sign.of_sort @{theory} (@{typ lam}, @{sort fs}) *}
thm lam_bp.fv[simplified lam_bp.supp(1-2)]
-equivariance alpha_lam_raw
end
--- a/Nominal/Ex/Ex2.thy Wed May 12 16:33:50 2010 +0100
+++ b/Nominal/Ex/Ex2.thy Wed May 12 16:59:53 2010 +0100
@@ -27,8 +27,6 @@
thm trm_pat.distinct
thm trm_pat.fv[simplified trm_pat.supp(1-2)]
-equivariance alpha_trm_raw
-
end
--- a/Nominal/Ex/Ex3.thy Wed May 12 16:33:50 2010 +0100
+++ b/Nominal/Ex/Ex3.thy Wed May 12 16:59:53 2010 +0100
@@ -31,8 +31,6 @@
thm trm_pat.fv[simplified trm_pat.supp(1-2)]
-equivariance alpha_trm_raw
-
end
--- a/Nominal/Ex/ExLet.thy Wed May 12 16:33:50 2010 +0100
+++ b/Nominal/Ex/ExLet.thy Wed May 12 16:59:53 2010 +0100
@@ -34,7 +34,6 @@
(*thm trm_lts.supp*)
thm trm_lts.fv[simplified trm_lts.supp(1-2)]
-equivariance alpha_bn_raw
primrec
permute_bn_raw
--- a/Nominal/Ex/ExLetMult.thy Wed May 12 16:33:50 2010 +0100
+++ b/Nominal/Ex/ExLetMult.thy Wed May 12 16:59:53 2010 +0100
@@ -22,7 +22,6 @@
thm trm_lts.induct
thm trm_lts.fv[simplified trm_lts.supp]
-equivariance alpha_trm_raw
end
--- a/Nominal/Ex/ExLetRec.thy Wed May 12 16:33:50 2010 +0100
+++ b/Nominal/Ex/ExLetRec.thy Wed May 12 16:59:53 2010 +0100
@@ -32,7 +32,6 @@
thm trm_lts.supp
thm trm_lts.fv[simplified trm_lts.supp]
-equivariance alpha_trm_raw
(* why is this not in HOL simpset? *)
lemma set_sub: "{a, b} - {b} = {a} - {b}"
--- a/Nominal/Ex/ExPS3.thy Wed May 12 16:33:50 2010 +0100
+++ b/Nominal/Ex/ExPS3.thy Wed May 12 16:59:53 2010 +0100
@@ -34,7 +34,7 @@
thm exp_pat.fv
thm exp_pat.supp(1-2)
-equivariance alpha_exp_raw
+
end
--- a/Nominal/Ex/ExPS6.thy Wed May 12 16:33:50 2010 +0100
+++ b/Nominal/Ex/ExPS6.thy Wed May 12 16:59:53 2010 +0100
@@ -32,7 +32,7 @@
thm exp_pat.distinct
thm exp_pat.supp
-equivariance alpha_exp_raw
+
end
--- a/Nominal/Ex/ExPS7.thy Wed May 12 16:33:50 2010 +0100
+++ b/Nominal/Ex/ExPS7.thy Wed May 12 16:59:53 2010 +0100
@@ -28,7 +28,6 @@
thm exp_lrb_lrbs.eq_iff
thm exp_lrb_lrbs.supp
-equivariance alpha_exp_raw
end
--- a/Nominal/Ex/ExPS8.thy Wed May 12 16:33:50 2010 +0100
+++ b/Nominal/Ex/ExPS8.thy Wed May 12 16:59:53 2010 +0100
@@ -49,7 +49,6 @@
thm exp_fnclause_fnclauses_lrb_lrbs_pat.fv
thm exp_fnclause_fnclauses_lrb_lrbs_pat.eq_iff
-equivariance alpha_exp_raw
end
--- a/Nominal/Ex/LF.thy Wed May 12 16:33:50 2010 +0100
+++ b/Nominal/Ex/LF.thy Wed May 12 16:59:53 2010 +0100
@@ -20,7 +20,6 @@
thm kind_ty_trm.supp
-equivariance alpha_trm_raw
--- a/Nominal/Ex/Lambda.thy Wed May 12 16:33:50 2010 +0100
+++ b/Nominal/Ex/Lambda.thy Wed May 12 16:59:53 2010 +0100
@@ -15,7 +15,6 @@
declare lam.perm[eqvt]
-equivariance alpha_lam_raw
section {* Strong Induction Principles*}
--- a/Nominal/Ex/Modules.thy Wed May 12 16:33:50 2010 +0100
+++ b/Nominal/Ex/Modules.thy Wed May 12 16:59:53 2010 +0100
@@ -68,7 +68,6 @@
thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.supp(1-3,5-7,9-10)
thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.fv[simplified mexp_body_defn_sexp_sbody_spec_ty_path_trm.supp(1-3,5-7,9-10)]
-equivariance alpha_trm_raw
end
--- a/Nominal/Ex/SingleLet.thy Wed May 12 16:33:50 2010 +0100
+++ b/Nominal/Ex/SingleLet.thy Wed May 12 16:59:53 2010 +0100
@@ -28,7 +28,6 @@
ML {* Sign.of_sort @{theory} (@{typ trm}, @{sort fs}) *}
thm trm_assg.fv[simplified trm_assg.supp(1-2)]
-equivariance alpha_trm_raw
end
--- a/Nominal/Ex/TypeSchemes.thy Wed May 12 16:33:50 2010 +0100
+++ b/Nominal/Ex/TypeSchemes.thy Wed May 12 16:59:53 2010 +0100
@@ -14,7 +14,6 @@
lemmas ty_tys_supp = ty_tys.fv[simplified ty_tys.supp]
-equivariance alpha_ty_raw
(* below we define manually the function for size *)
--- a/Nominal/Manual/Term4.thy Wed May 12 16:33:50 2010 +0100
+++ b/Nominal/Manual/Term4.thy Wed May 12 16:59:53 2010 +0100
@@ -65,6 +65,8 @@
(fn ctxt => snd (Local_Theory.note ((@{binding alpha4_eqvt}, []),
build_alpha_eqvts [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] (fn _ => alpha_eqvt_tac @{thm alpha_rtrm4_alpha_rtrm4_list.induct} @{thms perm_fixed alpha4_inj} ctxt 1) ctxt) ctxt))
*}
+
+
thm alpha4_eqvt
lemmas alpha4_eqvt_fixed = alpha4_eqvt(1)[simplified alpha_fix (*fv_fix*)]
--- a/Nominal/ROOT.ML Wed May 12 16:33:50 2010 +0100
+++ b/Nominal/ROOT.ML Wed May 12 16:59:53 2010 +0100
@@ -14,6 +14,6 @@
"Ex/ExPS3",
"Ex/ExPS7",
"Ex/CoreHaskell",
- "Ex/Test",
- "Manual/Term4"
+ "Ex/Test"(*,
+ "Manual/Term4"*)
];