qed_spec_mp moved to end of file
authorsandnerr
Mon Dec 09 19:07:26 1996 +0100 (1996-12-09)
changeset 23537405e3cac88a
parent 2352 562cb286138e
child 2354 b4a1e3306aa0
qed_spec_mp moved to end of file
src/HOLCF/ROOT.ML
     1.1 --- a/src/HOLCF/ROOT.ML	Mon Dec 09 16:51:14 1996 +0100
     1.2 +++ b/src/HOLCF/ROOT.ML	Mon Dec 09 19:07:26 1996 +0100
     1.3 @@ -10,10 +10,6 @@
     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";
    1.14 @@ -47,4 +43,8 @@
    1.15  print_depth 100;  
    1.16  make_html:=false;
    1.17  
    1.18 +fun qed_spec_mp name =
    1.19 +  let val thm = normalize_thm [RSspec,RSmp] (result())
    1.20 +  in bind_thm(name, thm) end;
    1.21 +
    1.22  val HOLCF_build_completed = (); (*indicate successful build*)