| changeset 15674 | 4a1d07bb53e2 |
| parent 15531 | 08c8dad8e399 |
| child 22591 | 7d1015d59f24 |
--- a/TFL/dcterm.ML Thu Apr 07 09:28:16 2005 +0200 +++ b/TFL/dcterm.ML Thu Apr 07 09:51:17 2005 +0200 @@ -71,7 +71,7 @@ (*--------------------------------------------------------------------------- - * SOME simple constructor functions. + * Some simple constructor functions. *---------------------------------------------------------------------------*) val mk_hol_const = Thm.cterm_of (Theory.sign_of HOL.thy) o Const;