# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1268012416 -3600
# Node ID 094811120a68a0e713d54cfddb4d3b6ad8916b63
# Parent  7b0c6d07a24edbd0323460eeb6373c22f983aea0
Undo effects of simp.

diff -r 7b0c6d07a24e -r 094811120a68 Nominal/Term1.thy
--- 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: