src/HOL/Predicate.thy
changeset 56212 3253aaf73a01
parent 56166 9a241bc276cd
child 56218 1c3f1f2431f9
     1.1 --- a/src/HOL/Predicate.thy	Tue Mar 18 21:02:33 2014 +0100
     1.2 +++ b/src/HOL/Predicate.thy	Tue Mar 18 22:11:46 2014 +0100
     1.3 @@ -83,11 +83,11 @@
     1.4  
     1.5  end
     1.6  
     1.7 -lemma eval_INFI [simp]:
     1.8 +lemma eval_INF [simp]:
     1.9    "eval (INFI A f) = INFI A (eval \<circ> f)"
    1.10    using eval_Inf [of "f ` A"] by simp
    1.11  
    1.12 -lemma eval_SUPR [simp]:
    1.13 +lemma eval_SUP [simp]:
    1.14    "eval (SUPR A f) = SUPR A (eval \<circ> f)"
    1.15    using eval_Sup [of "f ` A"] by simp
    1.16