simpdata.ML

--- a/simpdata.ML	Wed Jul 27 19:08:40 1994 +0200
+++ b/simpdata.ML	Tue Aug 02 16:43:39 1994 +0200
@@ -63,11 +63,11 @@
    "(!x.P) = P", "(? x.P) = P",
    "(P|Q --> R) = ((P-->R)&(Q-->R))" ];
 
+in
+
 val meta_obj_reflection = prove_goal HOL.thy "x==y ==> x=y"
   (fn [prem] => [rewtac prem, rtac refl 1]);
 
-in
-
 val eq_sym_conv = prover "(x=y) = (y=x)";
 
 val conj_assoc = prover "((P&Q)&R) = (P&(Q&R))";