--- a/src/HOL/HOL.ML Wed Aug 06 11:56:31 1997 +0200
+++ b/src/HOL/HOL.ML Wed Aug 06 11:57:20 1997 +0200
@@ -349,14 +349,11 @@
_ $ (Const("op -->",_)$_$_) => th RS mp
| _ => raise THM("RSmp",0,[th]));
-(*Used in qed_spec_mp, etc.*)
fun normalize_thm funs =
let fun trans [] th = th
| trans (f::fs) th = (trans funs (f th)) handle THM _ => trans fs th
in trans funs end;
-end;
-
fun qed_spec_mp name =
let val thm = normalize_thm [RSspec,RSmp] (result())
in bind_thm(name, thm) end;
@@ -367,6 +364,9 @@
fun qed_goalw_spec_mp name thy defs s p =
bind_thm (name, normalize_thm [RSspec,RSmp] (prove_goalw thy defs s p));
+end;
+
+
(*Thus, assignments to the references claset and simpset are recorded
with theory "HOL". These files cannot be loaded directly in ROOT.ML.*)
use "hologic.ML";
--- a/src/HOLCF/ax_ops/thy_axioms.ML Wed Aug 06 11:56:31 1997 +0200
+++ b/src/HOLCF/ax_ops/thy_axioms.ML Wed Aug 06 11:57:20 1997 +0200
@@ -3,12 +3,6 @@
Author: Tobias Mayr
Additional theory file section for HOLCF: axioms
-There's an elaborate but german description of this program
-and a short english description of the new sections,
-write to mayrt@informatik.tu-muenchen.de.
-
-TODO:
-
*)
(*** new section of HOLCF : axioms
@@ -213,4 +207,3 @@
val axioms_sections = [("axioms" , ext_axiom_decls)]
end; (* the structure *)
-
--- a/src/HOLCF/ax_ops/thy_ops.ML Wed Aug 06 11:56:31 1997 +0200
+++ b/src/HOLCF/ax_ops/thy_ops.ML Wed Aug 06 11:57:20 1997 +0200
@@ -3,13 +3,9 @@
Author: Tobias Mayr
Additional theory file section for HOLCF: ops
-There's an elaborate but german description of this program,
-write to mayrt@informatik.tu-muenchen.de.
-For a short english description of the new sections
-write to regensbu@informatik.tu-muenchen.de.
-TODO: maybe AST-representation with "op name" instead of _I_...
-
+TODO:
+ maybe AST-representation with "op name" instead of _I_...
*)
signature THY_OPS =
@@ -453,4 +449,3 @@
val ops_sections = [("ops" , ops_decls) ];
end; (* the structure ThyOps *)
-