Reformatting of SIMPLIFIER figure
authorlcp
Fri, 19 Nov 1993 12:54:16 +0100
changeset 133 2322fd6d57a1
parent 132 b5704e45d2d2
child 134 595fda4879b6
Reformatting of SIMPLIFIER figure
doc-src/Ref/simplifier.tex
--- 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