# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1273729278 -7200
# Node ID f435d8efd751d411bb3b66b281841ac0ea602b28
# Parent  2786ff1df475a4a16510ea8387d173d9c2a67f8f
Make Term4 use 'equivariance'.

diff -r 2786ff1df475 -r f435d8efd751 Nominal/Manual/Term4.thy
--- a/Nominal/Manual/Term4.thy	Wed May 12 16:59:53 2010 +0100
+++ b/Nominal/Manual/Term4.thy	Thu May 13 07:41:18 2010 +0200
@@ -61,14 +61,10 @@
     alpha_rtrm4 ("_ \<approx>4 _" [100, 100] 100)
 and alpha_rtrm4_list ("_ \<approx>4l _" [100, 100] 100)
 
-local_setup {*
-(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*)]
+declare perm_fixed[eqvt]
+equivariance alpha_rtrm4
+lemmas alpha4_eqvt = eqvts(1-2)
+lemmas alpha4_eqvt_fixed = alpha4_eqvt(2)[simplified alpha_fix (*fv_fix*)]
 
 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_reflp}, []),
   build_alpha_refl [((0, @{term alpha_rtrm4}), 0), ((0, @{term alpha_rtrm4_list}), 0)] [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] @{thm rtrm4.induct} @{thms alpha4_inj} ctxt) ctxt)) *}
@@ -163,8 +159,9 @@
   (flat (map (distinct_rel @{context} @{thms alpha_rtrm4.cases alpha_rtrm4_list.cases}) [(@{thms rtrm4.distinct},@{term "alpha_rtrm4"})]))
 *}
 
+thm eqvts(6-7)
 ML {*
-  map (lift_thm [@{typ trm4}] @{context}) @{thms eqvts(1-2)[simplified fv_fix]}
+  map (lift_thm [@{typ trm4}] @{context}) @{thms eqvts(6-7)[simplified fv_fix]}
 *}
 
 end