explicit is better than implicit;
authorwenzelm
Thu Feb 16 16:42:26 2012 +0100 (2012-02-16)
changeset 46503186f4cab2ba0
parent 46502 3d43d4d4d071
child 46505 cefceb54c656
explicit is better than implicit;
src/HOL/Tools/Meson/meson.ML
     1.1 --- a/src/HOL/Tools/Meson/meson.ML	Thu Feb 16 14:14:58 2012 +0100
     1.2 +++ b/src/HOL/Tools/Meson/meson.ML	Thu Feb 16 16:42:26 2012 +0100
     1.3 @@ -756,8 +756,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 = read_instantiate @{context} [(("R", 0), "False")] notE;
     1.8 -val notEfalse' = rotate_prems 1 notEfalse;
     1.9 +val notEfalse = @{lemma "~ P ==> P ==> False" by (rule notE)};
    1.10 +val notEfalse' = @{lemma "P ==> ~ P ==> False" by (rule notE)};
    1.11  
    1.12  fun negated_asm_of_head th =
    1.13      th RS notEfalse handle THM _ => th RS notEfalse';