Mercurial Mercurial > repos > isabelle / 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.
tuned
authorhaftmann
Sun, 04 Sep 2011 09:28:15 +0200
changeset 44830 f710ce327b08
parent 44696 4e99277c81f2
child 44831 4ea848959340
tuned
src/HOL/Nominal/nominal_permeq.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Nominal/nominal_permeq.ML	Sun Sep 04 08:43:06 2011 +0200
+++ b/src/HOL/Nominal/nominal_permeq.ML	Sun Sep 04 09:28:15 2011 +0200
@@ -130,7 +130,7 @@
      case redex of 
        (* case pi o f == (%x. pi o (f ((rev pi)o x))) *)     
        (Const("Nominal.perm",_) $ pi $ f)  => 
-          (if (applicable_fun f) then SOME perm_fun_def else NONE)
+          (if applicable_fun f then SOME perm_fun_def else NONE)
       | _ => NONE
    end
isabelle