added qed_spec_mp (from HOL);
authorwenzelm
Fri Nov 29 15:31:13 1996 +0100 (1996-11-29)
changeset 228290fb68d597f8
parent 2281 e00c13a29eda
child 2283 68829cf138fc
added qed_spec_mp (from HOL);
src/HOLCF/ROOT.ML
     1.1 --- a/src/HOLCF/ROOT.ML	Fri Nov 29 15:11:37 1996 +0100
     1.2 +++ b/src/HOLCF/ROOT.ML	Fri Nov 29 15:31:13 1996 +0100
     1.3 @@ -10,6 +10,10 @@
     1.4  val banner = "HOLCF with sections axioms,ops,domain,generated";
     1.5  init_thy_reader();
     1.6  
     1.7 +fun qed_spec_mp name =
     1.8 +  let val thm = normalize_thm [RSspec,RSmp] (result())
     1.9 +  in bind_thm(name, thm) end;
    1.10 +
    1.11  (* start 8bit 1 *)
    1.12  val banner = 
    1.13          "HOLCF with sections axioms,ops,domain,generated and 8bit characters";