diff -r 98236fbd8aa6 -r 25dcb2b1329e Nominal/Ex/CoreHaskell.thy
--- a/Nominal/Ex/CoreHaskell.thy	Fri Dec 03 13:51:07 2010 +0000
+++ b/Nominal/Ex/CoreHaskell.thy	Mon Dec 06 14:24:17 2010 +0000
@@ -86,6 +86,10 @@
 
 (* generated theorems *)
 
+thm core_haskell.perm_bn_alpha
+thm core_haskell.perm_bn_simps
+thm core_haskell.bn_finite
+
 thm core_haskell.distinct
 thm core_haskell.induct
 thm core_haskell.exhaust