doc-src/Ref/simplifier.tex
changeset 133 2322fd6d57a1
parent 122 db9043a8e372
child 286 e7efbf03562b
--- a/doc-src/Ref/simplifier.tex	Fri Nov 19 11:35:59 1993 +0100
+++ b/doc-src/Ref/simplifier.tex	Fri Nov 19 12:54:16 1993 +0100
@@ -174,10 +174,10 @@
   type simpset
   val simp_tac:          simpset -> int -> tactic
   val asm_simp_tac:      simpset -> int -> tactic
-  val asm_full_simp_tac: simpset -> int -> tactic
-  val addeqcongs:  simpset * thm list -> simpset
-  val addsimps:    simpset * thm list -> simpset
-  val delsimps:    simpset * thm list -> simpset
+  val asm_full_simp_tac: simpset -> int -> tactic\smallskip
+  val addeqcongs:   simpset * thm list -> simpset
+  val addsimps:     simpset * thm list -> simpset
+  val delsimps:     simpset * thm list -> simpset
   val empty_ss:     simpset
   val merge_ss:     simpset * simpset -> simpset
   val setsubgoaler: simpset * (simpset -> int -> tactic) -> simpset