src/Pure/drule.ML
changeset 28713 135317cd34d6
parent 28674 08a77c495dc1
child 29265 5b4247055bd7
equal deleted inserted replaced
28712:4f2954d995f0 28713:135317cd34d6
   582 
   582 
   583 (*** Some useful meta-theorems ***)
   583 (*** Some useful meta-theorems ***)
   584 
   584 
   585 (*The rule V/V, obtains assumption solving for eresolve_tac*)
   585 (*The rule V/V, obtains assumption solving for eresolve_tac*)
   586 val asm_rl = store_standard_thm_open "asm_rl" (Thm.trivial (read_prop "?psi"));
   586 val asm_rl = store_standard_thm_open "asm_rl" (Thm.trivial (read_prop "?psi"));
   587 val _ = store_thm "_" asm_rl;
   587 val _ = store_thm_open "_" asm_rl;
   588 
   588 
   589 (*Meta-level cut rule: [| V==>W; V |] ==> W *)
   589 (*Meta-level cut rule: [| V==>W; V |] ==> W *)
   590 val cut_rl =
   590 val cut_rl =
   591   store_standard_thm_open "cut_rl"
   591   store_standard_thm_open "cut_rl"
   592     (Thm.trivial (read_prop "?psi ==> ?theta"));
   592     (Thm.trivial (read_prop "?psi ==> ?theta"));