# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1274198201 -7200
# Node ID 8c24ee88b8e87ddd4f6330a802ba09b11e1b8a45
# Parent  ce00205e07abeedaabcf5af7c4286faabdbf825e
more on subst

diff -r ce00205e07ab -r 8c24ee88b8e8 Nominal/Ex/Lambda.thy
--- a/Nominal/Ex/Lambda.thy	Tue May 18 17:17:54 2010 +0200
+++ b/Nominal/Ex/Lambda.thy	Tue May 18 17:56:41 2010 +0200
@@ -508,6 +508,10 @@
 | "subst_raw (Lam_raw x t) y s =
      (if x = y then t else
        (if atom x \<notin> (fv_lam_raw s) then (Lam_raw x (subst_raw t y s)) else undefined))"
+(* termination/lifting fail with sth like:
+| "subst_raw (Lam_raw x t) y s =
+     (FRESH v. Lam_raw v (subst_raw (subst_var_raw t x v) y s))"
+*)
 
 quotient_definition
   subst ("_ [ _ ::= _ ]" [100,100,100] 100)