src/HOL/HOL.thy
changeset 60143 2cd31c81e0e7
parent 59990 a81dc82ecba3
child 60147 6d7b7a037e8d
     1.1 --- a/src/HOL/HOL.thy	Sun Apr 19 21:26:50 2015 +0200
     1.2 +++ b/src/HOL/HOL.thy	Wed Apr 22 12:11:48 2015 +0200
     1.3 @@ -1292,7 +1292,8 @@
     1.4  
     1.5  lemmas [simp] =
     1.6    triv_forall_equality (*prunes params*)
     1.7 -  True_implies_equals  (*prune asms `True'*)
     1.8 +  True_implies_equals implies_True_equals (*prune True in asms*)
     1.9 +  False_implies_equals (*prune False in asms*)
    1.10    if_True
    1.11    if_False
    1.12    if_cancel