# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1266483658 -3600
# Node ID 166cc41091b9306756c9847958522d2d9380b6df
# Parent  7566b899ca6a58878523f89b82f556b5b21941c3
The alternate version of trm5 with additional binding. All proofs work the same.

diff -r 7566b899ca6a -r 166cc41091b9 Quot/Nominal/Terms.thy
--- a/Quot/Nominal/Terms.thy	Thu Feb 18 09:46:38 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Thu Feb 18 10:00:58 2010 +0100
@@ -432,9 +432,17 @@
   "rbv5 rLnil = {}"
 | "rbv5 (rLcons n t ltl) = {atom n} \<union> (rbv5 ltl)"
 
+
+(*
 local_setup {* define_raw_fv "Terms.rtrm5" [
   [[[]], [[], []], [[(SOME @{term rbv5}, 0)], [(SOME @{term rbv5}, 0)]]], [[], [[], [], []]]  ] *}
 print_theorems
+*)
+(* Alternate version with additional binding of name in rlts in rLcons *)
+local_setup {* define_raw_fv "Terms.rtrm5" [
+  [[[]], [[], []], [[(SOME @{term rbv5}, 0)], [(SOME @{term rbv5}, 0)]]], [[], [[(NONE,0)], [], [(NONE,0)]]]  ] *}
+print_theorems
+
 
 setup {* snd o define_raw_perms ["rtrm5", "rlts"] ["Terms.rtrm5", "Terms.rlts"] *}
 print_theorems