# HG changeset patch
# User nipkow
# Date 775838619 -7200
# Node ID be01ba66ba7b0ff981c685e2d1dce2b772358937
# Parent  f353b187526a6135e28ffff8ca89190f4b2547bc
exposed meta_obj_reflection

diff -r f353b187526a -r be01ba66ba7b 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))";