# HG changeset patch # User Christian Urban # Date 1285418284 14400 # Node ID fbdaaa20396b993abf441453f31ff9d69fb9981b # Parent b4ea19604b0ba59e2845238685cd6e9bbc73148f lifted size_thms and exported them as .size diff -r b4ea19604b0b -r fbdaaa20396b Nominal/Ex/SingleLet.thy --- a/Nominal/Ex/SingleLet.thy Sat Sep 25 08:28:45 2010 -0400 +++ b/Nominal/Ex/SingleLet.thy Sat Sep 25 08:38:04 2010 -0400 @@ -35,7 +35,7 @@ thm single_let.supports thm single_let.fsupp thm single_let.supp - +thm single_let.size diff -r b4ea19604b0b -r fbdaaa20396b Nominal/Nominal2.thy --- a/Nominal/Nominal2.thy Sat Sep 25 08:28:45 2010 -0400 +++ b/Nominal/Nominal2.thy Sat Sep 25 08:38:04 2010 -0400 @@ -529,13 +529,14 @@ ||>> lift_thms qtys [] (raw_fv_eqvt @ raw_bn_eqvt) else raise TEST lthy9a - val (((qsize_eqvt, [qinduct]), qexhausts), lthyB) = + val ((((qsize_eqvt, [qinduct]), qexhausts), qsize_simps), lthyB) = if get_STEPS lthy > 27 then lthyA |> lift_thms qtys [] raw_size_eqvt ||>> lift_thms qtys [] [raw_induct_thm] ||>> lift_thms qtys [] raw_exhaust_thms + ||>> lift_thms qtys [] raw_size_thms else raise TEST lthyA val qinducts = Project_Rule.projections lthyA qinduct @@ -582,6 +583,7 @@ ||>> Local_Theory.note ((thms_suffix "bn_defs", []), qbn_defs) ||>> Local_Theory.note ((thms_suffix "perm_simps", [eqvt_attr, simp_attr]), qperm_simps) ||>> Local_Theory.note ((thms_suffix "fv_bn_eqvt", []), qfv_qbn_eqvts) + ||>> Local_Theory.note ((thms_suffix "size", []), qsize_simps) ||>> Local_Theory.note ((thms_suffix "size_eqvt", []), qsize_eqvt) ||>> Local_Theory.note ((thms_suffix "induct", []), [qinduct]) ||>> Local_Theory.note ((thms_suffix "inducts", []), qinducts)