# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1271326538 -7200
# Node ID 13bc3f41ad8d783e11cb445b2d7819a5d4692f18
# Parent  d25e1576ca82f1668840a8de8b4450219b5e515a
Updating in Term4.

diff -r d25e1576ca82 -r 13bc3f41ad8d Nominal/Manual/Term4.thy
--- a/Nominal/Manual/Term4.thy	Thu Apr 15 12:08:46 2010 +0200
+++ b/Nominal/Manual/Term4.thy	Thu Apr 15 12:15:38 2010 +0200
@@ -1,5 +1,5 @@
 theory Term4
-imports "../Abs" "../Perm" "../Fv" "../Rsp" "Quotient_List"
+imports "../Abs" "../Perm" "../Fv" "../Rsp" "../Lift" "Quotient_List"
 begin
 
 atom_decl name
@@ -29,8 +29,9 @@
 thm permute_rtrm4_permute_rtrm4_list.simps
 thm permute_rtrm4_permute_rtrm4_list.simps[simplified repaired]
 
-local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term4.rtrm4")
-  [[[], [], [(NONE, 0,1)]], [[], []]  ] *}
+ML define_fv_alpha_export
+local_setup {* snd o define_fv_alpha_export (Datatype.the_info @{theory} "Term4.rtrm4")
+  [[[], [], [(NONE, 0, 1, AlphaGen)]], [[], []] ] [] *}
 print_theorems
 
 lemma fix2: "alpha_rtrm4_list = list_rel alpha_rtrm4"
@@ -54,10 +55,10 @@
   alpha_rtrm4_list ("_ \<approx>4l _" [100, 100] 100)
 thm alpha_rtrm4_alpha_rtrm4_list.intros[simplified fix2]
 
-local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_inj}, []), (build_alpha_inj @{thms alpha_rtrm4_alpha_rtrm4_list.intros[simplified fix2]} @{thms rtrm4.distinct rtrm4.inject list.distinct list.inject} @{thms alpha_rtrm4.cases[simplified fix2] alpha_rtrm4_list.cases[simplified fix2]} ctxt)) ctxt)) *}
+local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_inj}, []), (build_rel_inj @{thms alpha_rtrm4_alpha_rtrm4_list.intros[simplified fix2]} @{thms rtrm4.distinct rtrm4.inject list.distinct list.inject} @{thms alpha_rtrm4.cases[simplified fix2] alpha_rtrm4_list.cases[simplified fix2]} ctxt)) ctxt)) *}
 thm alpha4_inj
 
-local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_inj_no}, []), (build_alpha_inj @{thms alpha_rtrm4_alpha_rtrm4_list.intros} @{thms rtrm4.distinct rtrm4.inject list.distinct list.inject} @{thms alpha_rtrm4.cases alpha_rtrm4_list.cases} ctxt)) ctxt)) *}
+local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_inj_no}, []), (build_rel_inj @{thms alpha_rtrm4_alpha_rtrm4_list.intros} @{thms rtrm4.distinct rtrm4.inject list.distinct list.inject} @{thms alpha_rtrm4.cases alpha_rtrm4_list.cases} ctxt)) ctxt)) *}
 thm alpha4_inj_no
 
 local_setup {*