Mercurial Mercurial > hg > nominal2 / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Nominal/Nominal2.thy
changeset 2617 e44551d067e6
parent 2616 dd7490fdd998
child 2618 d17fadc20507
equal deleted inserted replaced
2616:dd7490fdd998 2617:e44551d067e6 
   305         in
 
   305         in
 
   306           EVERY1 [Goal.conjunction_tac,
 
   306           EVERY1 [Goal.conjunction_tac,
 
   307             RANGE (map2 (case_tac context c bn_finite_thms eq_iff_thms bn_eqvt permute_bns perm_bn_alphas) 
   307             RANGE (map2 (case_tac context c bn_finite_thms eq_iff_thms bn_eqvt permute_bns perm_bn_alphas) 
   308                       (prems' ~~ bclausesss) exhausts')]
 
   308                       (prems' ~~ bclausesss) exhausts')]
 
   309         end)
 
   309         end)
 
       
   310     |> ProofContext.export lthy'' lthy
 
   310   end
 
   311   end
 
   311 *}
 
   312 *}
 
   312 
   313 
   313 
   314 
   314 
   315 
   845      ||>> Local_Theory.note ((thms_suffix "size", []), qsize_simps)
 
   846      ||>> Local_Theory.note ((thms_suffix "size", []), qsize_simps)
 
   846      ||>> Local_Theory.note ((thms_suffix "size_eqvt", []), qsize_eqvt)
 
   847      ||>> Local_Theory.note ((thms_suffix "size_eqvt", []), qsize_eqvt)
 
   847      ||>> Local_Theory.note ((thms_suffix "induct", []), [qinduct]) 
   848      ||>> Local_Theory.note ((thms_suffix "induct", []), [qinduct]) 
   848      ||>> Local_Theory.note ((thms_suffix "inducts", []), qinducts)
 
   849      ||>> Local_Theory.note ((thms_suffix "inducts", []), qinducts)
 
   849      ||>> Local_Theory.note ((thms_suffix "exhaust", []), qexhausts)
 
   850      ||>> Local_Theory.note ((thms_suffix "exhaust", []), qexhausts)
 
       
   851      ||>> Local_Theory.note ((thms_suffix "strong_exhaust", []), qstrong_exhaust_thms)
 
   850      ||>> Local_Theory.note ((thms_suffix "supports", []), qsupports_thms)
 
   852      ||>> Local_Theory.note ((thms_suffix "supports", []), qsupports_thms)
 
   851      ||>> Local_Theory.note ((thms_suffix "fsupp", []), qfsupp_thms)
 
   853      ||>> Local_Theory.note ((thms_suffix "fsupp", []), qfsupp_thms)
 
   852      ||>> Local_Theory.note ((thms_suffix "supp", []), qsupp_constrs)
 
   854      ||>> Local_Theory.note ((thms_suffix "supp", []), qsupp_constrs)
 
   853      ||>> Local_Theory.note ((thms_suffix "fresh", []), qfresh_constrs)
 
   855      ||>> Local_Theory.note ((thms_suffix "fresh", []), qfresh_constrs)
 
   854      ||>> Local_Theory.note ((thms_suffix "raw_alpha", []), alpha_intros)
 
   856      ||>> Local_Theory.note ((thms_suffix "raw_alpha", []), alpha_intros)
nominal2