Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
val rev_eq_reflection = def_imp_eq;
authorwenzelm
Fri, 04 Aug 2000 22:57:37 +0200
changeset 9531 7a0d4a6299b4
parent 9530 f0ffd29fd4e4
child 9532 36b9bc6eb454
val rev_eq_reflection = def_imp_eq;
src/HOL/cladata.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle