# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1273825722 -7200
# Node ID d74e08799b63b5ef4463d9e3d45311015f72114d
# Parent  f7ec6f7b152e2c550b2baf33f49734cb7854e7ef
SingleLetFoo with everything.

diff -r f7ec6f7b152e -r d74e08799b63 Nominal/Ex/SingleLetFoo.thy
--- a/Nominal/Ex/SingleLetFoo.thy	Fri May 14 10:21:14 2010 +0200
+++ b/Nominal/Ex/SingleLetFoo.thy	Fri May 14 10:28:42 2010 +0200
@@ -3,8 +3,7 @@
 begin
 
 
-declare [[STEPS = 4]]
-(* alpha does not work for this type *)
+declare [[STEPS = 5]]
 
 atom_decl name
 
@@ -22,6 +21,11 @@
 where
   "bn (As x t) = {atom x}"
 
+thm trm_assg.distinct
+thm trm_assg.eq_iff
+thm trm_assg.supp
+thm trm_assg.perm
+
 thm permute_trm_raw_permute_assg_raw.simps
 thm fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps[no_vars]