# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1257268199 -3600
# Node ID ddd2f209d0d29f54a27ce3576e752c1cada76a3c
# Parent  1b57f99737feb01a863b729ed6a4359474973751
Playing with alpha_refl.

diff -r 1b57f99737fe -r ddd2f209d0d2 LamEx.thy
--- a/LamEx.thy	Tue Nov 03 17:51:10 2009 +0100
+++ b/LamEx.thy	Tue Nov 03 18:09:59 2009 +0100
@@ -34,6 +34,10 @@
 
 lemma alpha_refl:
   shows "x \<approx> x"
+  apply (rule rlam.induct)
+  apply (simp_all add:a1 a2)
+  apply (rule a3)
+  apply (simp_all)
 sorry
 
 quotient lam = rlam / alpha