# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1289696456 0
# Node ID 7c8bfc35663a80552e875a7eab413c87aea57d9d
# Parent  e8ec504dddf209fec6662b36334d2dbf2fbad990
lifted permute_bn simp rules

diff -r e8ec504dddf2 -r 7c8bfc35663a Nominal/Nominal2.thy
--- a/Nominal/Nominal2.thy	Sat Nov 13 22:23:26 2010 +0000
+++ b/Nominal/Nominal2.thy	Sun Nov 14 01:00:56 2010 +0000
@@ -549,7 +549,7 @@
       ||>> lift_thms qtys [] (raw_fv_eqvt @ raw_bn_eqvt)
     else raise TEST lthy9a
 
-  val ((((qsize_eqvt, [qinduct]), qexhausts), qsize_simps), lthyB) = 
+  val (((((qsize_eqvt, [qinduct]), qexhausts), qsize_simps), qperm_bn_simps), lthyB) = 
     if get_STEPS lthy > 28
     then
       lthyA 
@@ -557,6 +557,7 @@
       ||>> lift_thms qtys [] [raw_induct_thm]
       ||>> lift_thms qtys [] raw_exhaust_thms
       ||>> lift_thms qtys [] raw_size_thms
+      ||>> lift_thms qtys [] raw_perm_bn_simps
     else raise TEST lthyA
 
   val qinducts = Project_Rule.projections lthyA qinduct
@@ -633,6 +634,7 @@
      ||>> Local_Theory.note ((thms_suffix "supp", []), qsupp_constrs)
      ||>> Local_Theory.note ((thms_suffix "fresh", []), qfresh_constrs)
      ||>> Local_Theory.note ((thms_suffix "raw_alpha", []), alpha_intros)
+     ||>> Local_Theory.note ((thms_suffix "perm_bn_simps", []), qperm_bn_simps)
 in
   (0, lthy9')
 end handle TEST ctxt => (0, ctxt)