Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
doc-src/Ref/substitution.tex
changeset 8136 8c65f3ca13f2
parent 6618 13293a7d4a57
child 9524 5721615da108 
--- a/doc-src/Ref/substitution.tex	Tue Jan 18 11:00:10 2000 +0100
+++ b/doc-src/Ref/substitution.tex	Tue Jan 18 11:33:31 2000 +0100
@@ -128,12 +128,12 @@
   val dest_Trueprop    : term -> term
   val dest_eq          : term -> term*term*typ
   val dest_imp         : term -> term*term
-  val eq_reflection    : thm             (* a=b ==> a==b *)
-  val imp_intr         : thm             (* (P ==> Q) ==> P-->Q *)
-  val rev_mp           : thm             (* [| P;  P-->Q |] ==> Q *)
-  val subst            : thm             (* [| a=b;  P(a) |] ==> P(b) *)
-  val sym              : thm             (* a=b ==> b=a *)
-  val thin_refl        : thm             (* [|x=x; P|] ==> P *)
+  val eq_reflection    : thm         (* a=b ==> a==b *)
+  val imp_intr         : thm         (*(P ==> Q) ==> P-->Q *)
+  val rev_mp           : thm         (* [| P;  P-->Q |] ==> Q *)
+  val subst            : thm         (* [| a=b;  P(a) |] ==> P(b) *)
+  val sym              : thm         (* a=b ==> b=a *)
+  val thin_refl        : thm         (* [|x=x; P|] ==> P *)
   end;
 \end{ttbox}
 Thus, the functor requires the following items:
isabelle