diff -r 8a4c44cef353 -r 16ffbc8442ca Nominal/Nominal2.thy
--- a/Nominal/Nominal2.thy	Thu Dec 23 01:05:05 2010 +0000
+++ b/Nominal/Nominal2.thy	Sun Dec 26 16:35:16 2010 +0000
@@ -529,9 +529,12 @@
     then prove_permute_bn_thms qtys qbns qperm_bns qinduct qperm_bn_simps qbn_defs qfv_qbn_eqvts lthyC
     else []
 
+  (* proving the strong exhausts and induct lemmas *)
   val qstrong_exhaust_thms = prove_strong_exhausts lthyC qexhausts bclauses qbn_finite_thms qeq_iffs'
     qfv_qbn_eqvts qpermute_bn_thms qperm_bn_alpha_thms
 
+  val qstrong_induct_thm = prove_strong_induct lthyC qinduct qexhausts bclauses
+
 
   (* noting the theorems *)