Mercurialisabelle / changeset
summary | shortlog | changelog | graph | tags | branches | files | changeset | raw | gz
tuned
authorhaftmann
Sun Sep 04 09:28:15 2011 +0200 (2011-09-04)
changeset 44830f710ce327b08
parent 44696 4e99277c81f2
child 44831 4ea848959340
tuned
src/HOL/Nominal/nominal_permeq.ML file | annotate | diff | revisions 
     1.1 --- a/src/HOL/Nominal/nominal_permeq.ML	Sun Sep 04 08:43:06 2011 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_permeq.ML	Sun Sep 04 09:28:15 2011 +0200
     1.3 @@ -130,7 +130,7 @@
     1.4       case redex of 
     1.5         (* case pi o f == (%x. pi o (f ((rev pi)o x))) *)     
     1.6         (Const("Nominal.perm",_) $ pi $ f)  => 
     1.7 -          (if (applicable_fun f) then SOME perm_fun_def else NONE)
     1.8 +          (if applicable_fun f then SOME perm_fun_def else NONE)
     1.9        | _ => NONE
    1.10     end
    1.11
isabelle