src/Pure/drule.ML
changeset 13368 8f8ba32d148b
parent 13325 5b5e12f0aee0
child 13389 0cbda884a7e5
     1.1 --- a/src/Pure/drule.ML	Tue Jul 16 18:26:52 2002 +0200
     1.2 +++ b/src/Pure/drule.ML	Tue Jul 16 18:37:03 2002 +0200
     1.3 @@ -77,6 +77,7 @@
     1.4    val triv_forall_equality: thm
     1.5    val swap_prems_rl     : thm
     1.6    val equal_intr_rule   : thm
     1.7 +  val equal_elim_rule1  : thm
     1.8    val inst              : string -> string -> thm -> thm
     1.9    val instantiate'      : ctyp option list -> cterm option list -> thm -> thm
    1.10    val incr_indexes_wrt  : int list -> ctyp list -> cterm list -> thm list -> thm -> thm
    1.11 @@ -667,6 +668,13 @@
    1.12        (implies_intr PQ (implies_intr QP (equal_intr (assume PQ) (assume QP))))
    1.13    end;
    1.14  
    1.15 +(* [| PROP ?phi == PROP ?psi; PROP ?phi |] ==> PROP ?psi *)
    1.16 +val equal_elim_rule1 =
    1.17 +  let val eq = read_prop "PROP phi == PROP psi"
    1.18 +      and P = read_prop "PROP phi"
    1.19 +  in store_standard_thm_open "equal_elim_rule1"
    1.20 +    (Thm.equal_elim (assume eq) (assume P) |> implies_intr_list [eq, P])
    1.21 +  end;
    1.22  
    1.23  (* "[| PROP ?phi; PROP ?phi; PROP ?psi |] ==> PROP ?psi" *)
    1.24