val rev_eq_reflection = def_imp_eq;
authorwenzelm
Fri Aug 04 22:57:37 2000 +0200 (2000-08-04)
changeset 95317a0d4a6299b4
parent 9530 f0ffd29fd4e4
child 9532 36b9bc6eb454
val rev_eq_reflection = def_imp_eq;
src/HOL/cladata.ML
     1.1 --- a/src/HOL/cladata.ML	Fri Aug 04 22:57:25 2000 +0200
     1.2 +++ b/src/HOL/cladata.ML	Fri Aug 04 22:57:37 2000 +0200
     1.3 @@ -18,6 +18,7 @@
     1.4    val dest_Trueprop = HOLogic.dest_Trueprop
     1.5    val dest_imp = HOLogic.dest_imp
     1.6    val eq_reflection = eq_reflection
     1.7 +  val rev_eq_reflection = def_imp_eq
     1.8    val imp_intr = impI
     1.9    val rev_mp = rev_mp
    1.10    val subst = subst