author haftmann Wed, 11 Oct 2006 14:51:41 +0200 changeset 20975 5bfa2e4ed789 parent 20974 2a29a21825d1 child 20976 e324808e9f1f
--- a/doc-src/Ref/substitution.tex	Wed Oct 11 14:51:25 2006 +0200
+++ b/doc-src/Ref/substitution.tex	Wed Oct 11 14:51:41 2006 +0200
@@ -126,7 +126,7 @@
sig
structure Simplifier : SIMPLIFIER
val dest_Trueprop    : term -> term
-  val dest_eq          : term -> term*term*typ
+  val dest_eq          : term -> (term*term)*typ
val dest_imp         : term -> term*term
val eq_reflection    : thm         (* a=b ==> a==b *)
val rev_eq_reflection: thm         (* a==b ==> a=b *)
@@ -146,7 +146,7 @@
corresponding object-level one.  Typically, it should return $P$ when
applied to the term $\texttt{Trueprop}\,P$ (see example below).

-\item[\ttindexbold{dest_eq}] should return the triple~$(t,u,T)$, where $T$ is
+\item[\ttindexbold{dest_eq}] should return the triple~$((t,u),T)$, where $T$ is
the type of~$t$ and~$u$, when applied to the \ML{} term that
represents~$t=u$.  For other terms, it should raise an exception.

@@ -188,7 +188,7 @@
fun dest_Trueprop (Const ("Trueprop", _) $P) = P | dest_Trueprop t = raise TERM ("dest_Trueprop", [t]); -fun dest_eq (Const("op =",T)$ t $u) = (t, u, domain_type T) +fun dest_eq (Const("op =",T)$ t $u) = ((t, u), domain_type T) fun dest_imp (Const("op -->",_)$ A \$ B) = (A, B)
| dest_imp  t = raise TERM ("dest_imp", [t]);