Mercurial Mercurial > hg > nominal2 / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Undo effects of simp.
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Mon, 08 Mar 2010 02:40:16 +0100
changeset 1356 094811120a68
parent 1355 7b0c6d07a24e
child 1357 42b7abf779ec
Undo effects of simp.
Nominal/Term1.thy file | annotate | diff | comparison | revisions 
--- a/Nominal/Term1.thy	Sun Mar 07 21:30:57 2010 +0100
+++ b/Nominal/Term1.thy	Mon Mar 08 02:40:16 2010 +0100
@@ -232,6 +232,7 @@
 apply(simp only: Un_commute)
 apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply(rule refl)
 apply(simp only: Collect_disj_eq[symmetric] inf_or)
+apply(simp only: HOL.imp_disj2[symmetric] HOL.not_ex[symmetric] HOL.disj_not1[symmetric] HOL.de_Morgan_conj[symmetric])
 sorry
 
 lemma supp_fv:
nominal2