src/Pure/drule.ML
changeset 7380 2bcee6a460d8
parent 7248 322151fe6f02
child 7404 e488cf3da60a
equal deleted inserted replaced
7379:999b1b777fc2 7380:2bcee6a460d8
   533 
   533 
   534 
   534 
   535 (*** Some useful meta-theorems ***)
   535 (*** Some useful meta-theorems ***)
   536 
   536 
   537 (*The rule V/V, obtains assumption solving for eresolve_tac*)
   537 (*The rule V/V, obtains assumption solving for eresolve_tac*)
   538 val asm_rl =
   538 val asm_rl = store_thm "asm_rl" (trivial(read_prop "PROP ?psi"));
   539   store_thm "asm_rl" (trivial(read_prop "PROP ?psi"));
   539 val _ = store_thm "_" asm_rl;
   540 
   540 
   541 (*Meta-level cut rule: [| V==>W; V |] ==> W *)
   541 (*Meta-level cut rule: [| V==>W; V |] ==> W *)
   542 val cut_rl =
   542 val cut_rl =
   543   store_thm "cut_rl"
   543   store_thm "cut_rl"
   544     (trivial(read_prop "PROP ?psi ==> PROP ?theta"));
   544     (trivial(read_prop "PROP ?psi ==> PROP ?theta"));