src/Pure/drule.ML
changeset 3653 6d5b3d5ff132
parent 3575 4e9beacb5339
child 3766 8e1794c4e81b
equal deleted inserted replaced
3652:4c484f03079c 3653:6d5b3d5ff132
    19   val cprems_of		: thm -> cterm list
    19   val cprems_of		: thm -> cterm list
    20   val cterm_instantiate	: (cterm*cterm)list -> thm -> thm
    20   val cterm_instantiate	: (cterm*cterm)list -> thm -> thm
    21   val cut_rl		: thm
    21   val cut_rl		: thm
    22   val equal_abs_elim	: cterm  -> thm -> thm
    22   val equal_abs_elim	: cterm  -> thm -> thm
    23   val equal_abs_elim_list: cterm list -> thm -> thm
    23   val equal_abs_elim_list: cterm list -> thm -> thm
       
    24   val equal_intr_rule   : thm
    24   val eq_thm		: thm * thm -> bool
    25   val eq_thm		: thm * thm -> bool
    25   val same_thm		: thm * thm -> bool
    26   val same_thm		: thm * thm -> bool
    26   val eq_thm_sg		: thm * thm -> bool
    27   val eq_thm_sg		: thm * thm -> bool
    27   val flexpair_abs_elim_list: cterm list -> thm -> thm
    28   val flexpair_abs_elim_list: cterm list -> thm -> thm
    28   val forall_intr_list	: cterm list -> thm -> thm
    29   val forall_intr_list	: cterm list -> thm -> thm
   656   in standard
   657   in standard
   657        (implies_intr cmajor (implies_intr cminor2 (implies_intr cminor1
   658        (implies_intr cmajor (implies_intr cminor2 (implies_intr cminor1
   658          (implies_elim (implies_elim major minor1) minor2))))
   659          (implies_elim (implies_elim major minor1) minor2))))
   659   end;
   660   end;
   660 
   661 
       
   662 (* [| PROP ?phi ==> PROP ?psi; PROP ?psi ==> PROP ?phi |]
       
   663    ==> PROP ?phi == PROP ?psi
       
   664    Introduction rule for == using ==> not meta-hyps.
       
   665 *)
       
   666 val equal_intr_rule =
       
   667   let val PQ = read_cterm Sign.proto_pure ("PROP phi ==> PROP psi", propT)
       
   668       and QP = read_cterm Sign.proto_pure ("PROP psi ==> PROP phi", propT)
       
   669   in  equal_intr (assume PQ) (assume QP)
       
   670       |> implies_intr QP
       
   671       |> implies_intr PQ
       
   672       |> standard
       
   673   end;
       
   674 
   661 end;
   675 end;
   662 
   676 
   663 open Drule;
   677 open Drule;