src/HOLCF/ROOT.ML
changeset 2282 90fb68d597f8
parent 2278 d63ffafce255
child 2353 7405e3cac88a
     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";