src/Pure/simplifier.ML
changeset 23598 e03a43b8178c
parent 23536 60a1672e298e
child 23655 d2d1138e0ddc
     1.1 --- a/src/Pure/simplifier.ML	Thu Jul 05 20:01:34 2007 +0200
     1.2 +++ b/src/Pure/simplifier.ML	Thu Jul 05 20:01:35 2007 +0200
     1.3 @@ -55,11 +55,11 @@
     1.4      -> (theory -> simpset -> term -> thm option) -> simproc
     1.5    val simproc: theory -> string -> string list
     1.6      -> (theory -> simpset -> term -> thm option) -> simproc
     1.7 -  val          rewrite: simpset -> cterm -> thm
     1.8 -  val      asm_rewrite: simpset -> cterm -> thm
     1.9 -  val     full_rewrite: simpset -> cterm -> thm
    1.10 -  val   asm_lr_rewrite: simpset -> cterm -> thm
    1.11 -  val asm_full_rewrite: simpset -> cterm -> thm
    1.12 +  val          rewrite: simpset -> conv
    1.13 +  val      asm_rewrite: simpset -> conv
    1.14 +  val     full_rewrite: simpset -> conv
    1.15 +  val   asm_lr_rewrite: simpset -> conv
    1.16 +  val asm_full_rewrite: simpset -> conv
    1.17    val get_simpset: theory -> simpset
    1.18    val print_local_simpset: Proof.context -> unit
    1.19    val get_local_simpset: Proof.context -> simpset