# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1273679993 -3600
# Node ID 2786ff1df475a4a16510ea8387d173d9c2a67f8f
# Parent  238062c4c9f2b4c1641efd5bb91956a937dd37d3
fixed the examples for the new eqvt-procedure....temporarily disabled Manual/Term4.thy

diff -r 238062c4c9f2 -r 2786ff1df475 Nominal/Ex/Classical.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
 
 
diff -r 238062c4c9f2 -r 2786ff1df475 Nominal/Ex/CoreHaskell.thy
--- 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
 
diff -r 238062c4c9f2 -r 2786ff1df475 Nominal/Ex/Ex1rec.thy
--- 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
diff -r 238062c4c9f2 -r 2786ff1df475 Nominal/Ex/Ex2.thy
--- 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
 
diff -r 238062c4c9f2 -r 2786ff1df475 Nominal/Ex/Ex3.thy
--- 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
 
diff -r 238062c4c9f2 -r 2786ff1df475 Nominal/Ex/ExLet.thy
--- 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
diff -r 238062c4c9f2 -r 2786ff1df475 Nominal/Ex/ExLetMult.thy
--- 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
diff -r 238062c4c9f2 -r 2786ff1df475 Nominal/Ex/ExLetRec.thy
--- 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}"
diff -r 238062c4c9f2 -r 2786ff1df475 Nominal/Ex/ExPS3.thy
--- 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
diff -r 238062c4c9f2 -r 2786ff1df475 Nominal/Ex/ExPS6.thy
--- 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
diff -r 238062c4c9f2 -r 2786ff1df475 Nominal/Ex/ExPS7.thy
--- 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
 
diff -r 238062c4c9f2 -r 2786ff1df475 Nominal/Ex/ExPS8.thy
--- 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
 
 
diff -r 238062c4c9f2 -r 2786ff1df475 Nominal/Ex/LF.thy
--- 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
 
 
 
diff -r 238062c4c9f2 -r 2786ff1df475 Nominal/Ex/Lambda.thy
--- 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*}
 
diff -r 238062c4c9f2 -r 2786ff1df475 Nominal/Ex/Modules.thy
--- 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
diff -r 238062c4c9f2 -r 2786ff1df475 Nominal/Ex/SingleLet.thy
--- 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
diff -r 238062c4c9f2 -r 2786ff1df475 Nominal/Ex/TypeSchemes.thy
--- 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 *)
diff -r 238062c4c9f2 -r 2786ff1df475 Nominal/Manual/Term4.thy
--- 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*)]
 
diff -r 238062c4c9f2 -r 2786ff1df475 Nominal/ROOT.ML
--- 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"*)
     ];