Tutorial/Minimal.thy
changeset 2686 52e1e98edb34
parent 2681 0e4c5fa26fa1
child 3132 87eca760dcba
--- a/Tutorial/Minimal.thy	Wed Jan 19 19:41:50 2011 +0100
+++ b/Tutorial/Minimal.thy	Wed Jan 19 23:58:12 2011 +0100
@@ -9,6 +9,8 @@
 | App "lam" "lam"
 | Lam x::"name" l::"lam"  bind x in l ("Lam [_]. _" [100, 100] 100)
 
+
+
 lemma alpha_test:
   shows "Lam [x]. (Var x) = Lam [y]. (Var y)"
   by (simp add: lam.eq_iff Abs1_eq_iff lam.fresh fresh_at_base)