Reformatting of SIMPLIFIER figure
authorlcp
Fri Nov 19 12:54:16 1993 +0100 (1993-11-19)
changeset 1332322fd6d57a1
parent 132 b5704e45d2d2
child 134 595fda4879b6
Reformatting of SIMPLIFIER figure
doc-src/Ref/simplifier.tex
     1.1 --- a/doc-src/Ref/simplifier.tex	Fri Nov 19 11:35:59 1993 +0100
     1.2 +++ b/doc-src/Ref/simplifier.tex	Fri Nov 19 12:54:16 1993 +0100
     1.3 @@ -174,10 +174,10 @@
     1.4    type simpset
     1.5    val simp_tac:          simpset -> int -> tactic
     1.6    val asm_simp_tac:      simpset -> int -> tactic
     1.7 -  val asm_full_simp_tac: simpset -> int -> tactic
     1.8 -  val addeqcongs:  simpset * thm list -> simpset
     1.9 -  val addsimps:    simpset * thm list -> simpset
    1.10 -  val delsimps:    simpset * thm list -> simpset
    1.11 +  val asm_full_simp_tac: simpset -> int -> tactic\smallskip
    1.12 +  val addeqcongs:   simpset * thm list -> simpset
    1.13 +  val addsimps:     simpset * thm list -> simpset
    1.14 +  val delsimps:     simpset * thm list -> simpset
    1.15    val empty_ss:     simpset
    1.16    val merge_ss:     simpset * simpset -> simpset
    1.17    val setsubgoaler: simpset * (simpset -> int -> tactic) -> simpset