src/FOL/IFOL.thy
changeset 11848 6e3017adb8c0
parent 11771 b7b100a2de1d
child 11953 f98623fdf6ef
     1.1 --- a/src/FOL/IFOL.thy	Sat Oct 20 20:18:19 2001 +0200
     1.2 +++ b/src/FOL/IFOL.thy	Sat Oct 20 20:18:45 2001 +0200
     1.3 @@ -160,4 +160,27 @@
     1.4  
     1.5  declare atomize_all [symmetric, rulify]  atomize_imp [symmetric, rulify]
     1.6  
     1.7 +
     1.8 +subsection {* Calculational rules *}
     1.9 +
    1.10 +lemma forw_subst: "a = b ==> P(b) ==> P(a)"
    1.11 +  by (rule ssubst)
    1.12 +
    1.13 +lemma back_subst: "P(a) ==> a = b ==> P(b)"
    1.14 +  by (rule subst)
    1.15 +
    1.16 +text {*
    1.17 +  Note that this list of rules is in reverse order of priorities.
    1.18 +*}
    1.19 +
    1.20 +lemmas trans_rules [trans] =
    1.21 +  forw_subst
    1.22 +  back_subst
    1.23 +  rev_mp
    1.24 +  mp
    1.25 +  transitive
    1.26 +  trans
    1.27 +
    1.28 +lemmas [Pure.elim] = sym
    1.29 +
    1.30  end