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.
fixed bug in simproc (also in the exec-version)
authorChristian Urban <urbanc@in.tum.de>
Fri, 25 May 2012 15:46:48 +0100
changeset 3176 31372760c2fb
parent 3175 52730e5ec8cb
child 3177 c25e4c9481f2
fixed bug in simproc (also in the exec-version)
Nominal/Nominal2_Base.thy file | annotate | diff | comparison | revisions
Nominal/Nominal2_Base_Exec.thy file | annotate | diff | comparison | revisions 
--- a/Nominal/Nominal2_Base.thy	Thu May 24 10:17:32 2012 +0200
+++ b/Nominal/Nominal2_Base.thy	Fri May 25 15:46:48 2012 +0100
@@ -2827,7 +2827,7 @@
              _ $ (@{term "HOL.Not"} $ (Const ("HOL.eq", _) $ l $ r)) =>
                (if l = lhs andalso r = rhs then SOME(thm)
                 else if r = lhs andalso l = rhs then SOME(thm RS @{thm not_sym})
-                else NONE)  
+                else first_is_neg lhs rhs thms)  
            | _ => first_is_neg lhs rhs thms)
 
     val simp_thms = @{thms fresh_Pair fresh_at_base atom_eq_iff}
--- a/Nominal/Nominal2_Base_Exec.thy	Thu May 24 10:17:32 2012 +0200
+++ b/Nominal/Nominal2_Base_Exec.thy	Fri May 25 15:46:48 2012 +0100
@@ -2735,7 +2735,7 @@
              _ $ (@{term "HOL.Not"} $ (Const ("HOL.eq", _) $ l $ r)) =>
                (if l = lhs andalso r = rhs then SOME(thm)
                 else if r = lhs andalso l = rhs then SOME(thm RS @{thm not_sym})
-                else NONE)
+                else first_is_neg lhs rhs thms)
            | _ => first_is_neg lhs rhs thms)
 
     val simp_thms = @{thms fresh_Pair fresh_at_base atom_eq_iff}
nominal2