Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
standard spelling: type-checking
authorpaulson
Wed, 03 Feb 1999 13:29:24 +0100
changeset 6172 8a505e0694d0
parent 6171 cd237a10cbf8
child 6173 2c0579e8e6fa
standard spelling: type-checking
src/ZF/Tools/inductive_package.ML file | annotate | diff | comparison | revisions 
--- a/src/ZF/Tools/inductive_package.ML	Wed Feb 03 13:26:07 1999 +0100
+++ b/src/ZF/Tools/inductive_package.ML	Wed Feb 03 13:29:24 1999 +0100
@@ -228,7 +228,7 @@
      rewrite_goals_tac con_defs,
      REPEAT (rtac refl 2),
      (*Typechecking; this can fail*)
-     if !Ind_Syntax.trace then print_tac "The typechecking subgoal:"
+     if !Ind_Syntax.trace then print_tac "The type-checking subgoal:"
      else all_tac,
      REPEAT (FIRSTGOAL (        dresolve_tac rec_typechecks
 			ORELSE' eresolve_tac (asm_rl::PartE::SigmaE2::
isabelle