src/HOL/Tools/Meson/meson.ML
changeset 46503 186f4cab2ba0
parent 46093 4bf24b90703c
child 46818 2a28e66e2e4c
equal deleted inserted replaced
46502:3d43d4d4d071 46503:186f4cab2ba0
   754   with no contrapositives, for ordinary resolution.*)
   754   with no contrapositives, for ordinary resolution.*)
   755 
   755 
   756 (*Rules to convert the head literal into a negated assumption. If the head
   756 (*Rules to convert the head literal into a negated assumption. If the head
   757   literal is already negated, then using notEfalse instead of notEfalse'
   757   literal is already negated, then using notEfalse instead of notEfalse'
   758   prevents a double negation.*)
   758   prevents a double negation.*)
   759 val notEfalse = read_instantiate @{context} [(("R", 0), "False")] notE;
   759 val notEfalse = @{lemma "~ P ==> P ==> False" by (rule notE)};
   760 val notEfalse' = rotate_prems 1 notEfalse;
   760 val notEfalse' = @{lemma "P ==> ~ P ==> False" by (rule notE)};
   761 
   761 
   762 fun negated_asm_of_head th =
   762 fun negated_asm_of_head th =
   763     th RS notEfalse handle THM _ => th RS notEfalse';
   763     th RS notEfalse handle THM _ => th RS notEfalse';
   764 
   764 
   765 (*Converting one theorem from a disjunction to a meta-level clause*)
   765 (*Converting one theorem from a disjunction to a meta-level clause*)