# HG changeset patch
# User wenzelm
# Date 965422657 -7200
# Node ID 7a0d4a6299b4dc82299fc500dc31d437551eb951
# Parent  f0ffd29fd4e41cf363868e227c4ef144c5edc39f
val rev_eq_reflection = def_imp_eq;

diff -r f0ffd29fd4e4 -r 7a0d4a6299b4 src/HOL/cladata.ML
--- a/src/HOL/cladata.ML	Fri Aug 04 22:57:25 2000 +0200
+++ b/src/HOL/cladata.ML	Fri Aug 04 22:57:37 2000 +0200
@@ -18,6 +18,7 @@
   val dest_Trueprop = HOLogic.dest_Trueprop
   val dest_imp = HOLogic.dest_imp
   val eq_reflection = eq_reflection
+  val rev_eq_reflection = def_imp_eq
   val imp_intr = impI
   val rev_mp = rev_mp
   val subst = subst