# HG changeset patch # User wenzelm # Date 1329406946 -3600 # Node ID 186f4cab2ba09910b4a5fa586445183120a8eecc # Parent 3d43d4d4d071a204fe8d34e8c83325b0d9453ac3 explicit is better than implicit; diff -r 3d43d4d4d071 -r 186f4cab2ba0 src/HOL/Tools/Meson/meson.ML --- a/src/HOL/Tools/Meson/meson.ML Thu Feb 16 14:14:58 2012 +0100 +++ b/src/HOL/Tools/Meson/meson.ML Thu Feb 16 16:42:26 2012 +0100 @@ -756,8 +756,8 @@ (*Rules to convert the head literal into a negated assumption. If the head literal is already negated, then using notEfalse instead of notEfalse' prevents a double negation.*) -val notEfalse = read_instantiate @{context} [(("R", 0), "False")] notE; -val notEfalse' = rotate_prems 1 notEfalse; +val notEfalse = @{lemma "~ P ==> P ==> False" by (rule notE)}; +val notEfalse' = @{lemma "P ==> ~ P ==> False" by (rule notE)}; fun negated_asm_of_head th = th RS notEfalse handle THM _ => th RS notEfalse';