# HG changeset patch
# User wenzelm
# Date 849277873 -3600
# Node ID 90fb68d597f8955e6c85baa6f4305ed59da626d7
# Parent  e00c13a29eda8a923ac171571c8a1145dc729abf
added qed_spec_mp (from HOL);

diff -r e00c13a29eda -r 90fb68d597f8 src/HOLCF/ROOT.ML
--- a/src/HOLCF/ROOT.ML	Fri Nov 29 15:11:37 1996 +0100
+++ b/src/HOLCF/ROOT.ML	Fri Nov 29 15:31:13 1996 +0100
@@ -10,6 +10,10 @@
 val banner = "HOLCF with sections axioms,ops,domain,generated";
 init_thy_reader();
 
+fun qed_spec_mp name =
+  let val thm = normalize_thm [RSspec,RSmp] (result())
+  in bind_thm(name, thm) end;
+
 (* start 8bit 1 *)
 val banner = 
         "HOLCF with sections axioms,ops,domain,generated and 8bit characters";