src/HOL/Set.thy
changeset 15524 2ef571f80a55
parent 15206 09d78ec709c7
child 15535 a0cf3a19ee36
     1.1 --- a/src/HOL/Set.thy	Thu Feb 10 17:09:15 2005 +0100
     1.2 +++ b/src/HOL/Set.thy	Thu Feb 10 18:51:12 2005 +0100
     1.3 @@ -6,7 +6,7 @@
     1.4  header {* Set theory for higher-order logic *}
     1.5  
     1.6  theory Set
     1.7 -imports HOL
     1.8 +imports Orderings
     1.9  begin
    1.10  
    1.11  text {* A set in HOL is simply a predicate. *}
    1.12 @@ -2057,12 +2057,6 @@
    1.13  
    1.14  subsection {* Transitivity rules for calculational reasoning *}
    1.15  
    1.16 -lemma forw_subst: "a = b ==> P b ==> P a"
    1.17 -  by (rule ssubst)
    1.18 -
    1.19 -lemma back_subst: "P a ==> a = b ==> P b"
    1.20 -  by (rule subst)
    1.21 -
    1.22  lemma set_rev_mp: "x:A ==> A \<subseteq> B ==> x:B"
    1.23    by (rule subsetD)
    1.24