Nominal/Ex/CoreHaskell.thy
changeset 2309 13f20fe02ff3
parent 2308 387fcbd33820
child 2311 4da5c5c29009
--- a/Nominal/Ex/CoreHaskell.thy	Wed Jun 02 11:37:51 2010 +0200
+++ b/Nominal/Ex/CoreHaskell.thy	Thu Jun 03 11:48:44 2010 +0200
@@ -8,7 +8,7 @@
 atom_decl cvar
 atom_decl tvar
 
-declare [[STEPS = 4]]
+declare [[STEPS = 9]]
 
 nominal_datatype tkind =
   KStar
@@ -83,8 +83,7 @@
 | "bv_tvs TvsNil = []"
 | "bv_tvs (TvsCons v k t) = (atom v) # bv_tvs t"
 | "bv_cvs CvsNil = []"
-| "bv_cvs (CvsCons v k t) = (atom v) # bv_cvs t"    
- 
+| "bv_cvs (CvsCons v k t) = (atom v) # bv_cvs t"
 
 
 lemmas fv_supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.supp(1-9,11,13,15)