# HG changeset patch
# User wenzelm
# Date 870861440 -7200
# Node ID d3e24885342886abaf9fd166d32895dac2dbf546
# Parent  ed1416badb41af00e16986a84929b1846c0f08ab
tuned comments;

diff -r ed1416badb41 -r d3e248853428 src/HOL/HOL.ML
--- 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";
diff -r ed1416badb41 -r d3e248853428 src/HOLCF/ax_ops/thy_axioms.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 *)
-
diff -r ed1416badb41 -r d3e248853428 src/HOLCF/ax_ops/thy_ops.ML
--- 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 *)
-