# HG changeset patch # User Cezary Kaliszyk # Date 1269591803 -3600 # Node ID 3b9c05d158f393455d77068005fa622e46e71ec9 # Parent f731e9aff8664b34468979735529824036f2d30f Fix Manual/LamEx for experiments. diff -r f731e9aff866 -r 3b9c05d158f3 Nominal/Manual/LamEx.thy --- a/Nominal/Manual/LamEx.thy Thu Mar 25 20:12:57 2010 +0100 +++ b/Nominal/Manual/LamEx.thy Fri Mar 26 09:23:23 2010 +0100 @@ -1,5 +1,5 @@ theory LamEx -imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" +imports "../Nominal2_Atoms" "../Nominal2_Eqvt" "../Nominal2_Supp" "../Abs" begin atom_decl name @@ -87,12 +87,12 @@ done inductive - alpha :: "rlam \ rlam \ bool" ("_ \ _" [100, 100] 100) + alpha :: "rlam \ rlam \ bool" ("_ \a _" [100, 100] 100) where - a1: "a = b \ (rVar a) \ (rVar b)" -| a2: "\t1 \ t2; s1 \ s2\ \ rApp t1 s1 \ rApp t2 s2" -| a3: "\pi. (rfv t - {atom a} = rfv s - {atom b} \ (rfv t - {atom a})\* pi \ (pi \ t) \ s) - \ rLam a t \ rLam b s" + a1: "a = b \ (rVar a) \a (rVar b)" +| a2: "\t1 \a t2; s1 \a s2\ \ rApp t1 s1 \a rApp t2 s2" +| a3: "\pi. (rfv t - {atom a} = rfv s - {atom b} \ (rfv t - {atom a})\* pi \ (pi \ t) \a s) + \ rLam a t \a rLam b s" lemma a3_inverse: assumes "rLam a t \ rLam b s"