doc-src/IsarRef/Thy/Inner_Syntax.thy

 
   These diagnostic commands assist interactive development by printing
   internal logical entities in a human-readable fashion.
 
   @{rail "
-    @@{command typ} @{syntax modes}? @{syntax type}
+    @@{command typ} @{syntax modes}? @{syntax type} ('::' @{syntax sort})?
     ;
     @@{command term} @{syntax modes}? @{syntax term}
     ;
     @@{command prop} @{syntax modes}? @{syntax prop}
     ;

     @{syntax_def modes}: '(' (@{syntax name} + ) ')'
   "}
 
   \begin{description}
 
-  \item @{command "typ"}~@{text \<tau>} reads and prints types of the
-  meta-logic according to the current theory or proof context.
+  \item @{command "typ"}~@{text \<tau>} reads and prints a type expression
+  according to the current context.
+
+  \item @{command "typ"}~@{text "\<tau> :: s"} uses type-inference to
+  determine the most general way to make @{text "\<tau>"} conform to sort
+  @{text "s"}.  For concrete @{text "\<tau>"} this checks if the type
+  belongs to that sort.  Dummy type parameters ``@{text "_"}''
+  (underscore) are assigned to fresh type variables with most general
+  sorts, according the the principles of type-inference.
 
   \item @{command "term"}~@{text t} and @{command "prop"}~@{text \<phi>}
   read, type-check and print terms or propositions according to the
   current theory or proof context; the inferred type of @{text t} is
   output as well.  Note that these commands are also useful in