--- a/src/FOL/IFOL.thy Sat Oct 20 20:18:19 2001 +0200
+++ b/src/FOL/IFOL.thy Sat Oct 20 20:18:45 2001 +0200
@@ -160,4 +160,27 @@
declare atomize_all [symmetric, rulify] atomize_imp [symmetric, rulify]
+
+subsection {* Calculational rules *}
+
+lemma forw_subst: "a = b ==> P(b) ==> P(a)"
+ by (rule ssubst)
+
+lemma back_subst: "P(a) ==> a = b ==> P(b)"
+ by (rule subst)
+
+text {*
+ Note that this list of rules is in reverse order of priorities.
+*}
+
+lemmas trans_rules [trans] =
+ forw_subst
+ back_subst
+ rev_mp
+ mp
+ transitive
+ trans
+
+lemmas [Pure.elim] = sym
+
end