ex/PropLog.ML

--- a/ex/PropLog.ML	Wed Dec 14 10:32:07 1994 +0100
+++ b/ex/PropLog.ML	Wed Dec 14 11:17:18 1994 +0100
@@ -26,7 +26,7 @@
 (* "[| G<=H;  G |- p |] ==> H |- p"
    This order of premises is convenient with RS
 *)
-val weaken_left = standard (thms_mono RS subsetD);
+bind_thm ("weaken_left", (thms_mono RS subsetD));
 
 (* H |- p ==> insert(a,H) |- p *)
 val weaken_left_insert = subset_insertI RS weaken_left;
@@ -58,7 +58,7 @@
 val thms_falseE = weaken_right RS (thms.DN RS thms.MP);
 
 (* [| H |- p->false;  H |- p;  q: pl |] ==> H |- q *)
-val thms_notE = standard (thms.MP RS thms_falseE);
+bind_thm ("thms_notE", (thms.MP RS thms_falseE));
 
 (** The function eval **)