# HG changeset patch # User nipkow # Date 769763043 -7200 # Node ID 432bb99958939c5b4462f41e560b858cadf9c416 # Parent 02b27671b899e403403003778afcbd0f8525b30b Modified mk_meta_eq to leave meta-equlities on unchanged. Thus you may now add ==-thms to simpsets. diff -r 02b27671b899 -r 432bb9995893 src/FOL/simpdata.ML --- a/src/FOL/simpdata.ML Thu May 19 17:06:24 1994 +0200 +++ b/src/FOL/simpdata.ML Tue May 24 09:04:03 1994 +0200 @@ -72,7 +72,8 @@ (*Make meta-equalities. The operator below is Trueprop*) fun mk_meta_eq th = case concl_of th of - _ $ (Const("op =",_)$_$_) => th RS eq_reflection + Const("==",_)$_$_ => th + | _ $ (Const("op =",_)$_$_) => th RS eq_reflection | _ $ (Const("op <->",_)$_$_) => th RS iff_reflection | _ $ (Const("Not",_)$_) => th RS iff_reflection_F | _ => th RS iff_reflection_T;