src/HOL/Tools/Meson/meson.ML
changeset 67091 1393c2340eec
parent 61268 abe08fb15a12
child 67149 e61557884799
     1.1 --- a/src/HOL/Tools/Meson/meson.ML	Sun Nov 26 13:19:52 2017 +0100
     1.2 +++ b/src/HOL/Tools/Meson/meson.ML	Sun Nov 26 21:08:32 2017 +0100
     1.3 @@ -770,8 +770,8 @@
     1.4  (*Rules to convert the head literal into a negated assumption. If the head
     1.5    literal is already negated, then using notEfalse instead of notEfalse'
     1.6    prevents a double negation.*)
     1.7 -val notEfalse = @{lemma "~ P ==> P ==> False" by (rule notE)};
     1.8 -val notEfalse' = @{lemma "P ==> ~ P ==> False" by (rule notE)};
     1.9 +val notEfalse = @{lemma "\<not> P \<Longrightarrow> P \<Longrightarrow> False" by (rule notE)};
    1.10 +val notEfalse' = @{lemma "P \<Longrightarrow> \<not> P \<Longrightarrow> False" by (rule notE)};
    1.11  
    1.12  fun negated_asm_of_head th =
    1.13      th RS notEfalse handle THM _ => th RS notEfalse';