628 The notational change from the ASCII character~\verb,%, to the |
628 The notational change from the ASCII character~\verb,%, to the |
629 symbol~@{text \<lambda>} reveals that Isabelle printed this term, after |
629 symbol~@{text \<lambda>} reveals that Isabelle printed this term, after |
630 parsing and type-checking. Document preparation enables symbolic |
630 parsing and type-checking. Document preparation enables symbolic |
631 output by default. |
631 output by default. |
632 |
632 |
633 \medskip The next example includes an option to modify Isabelle's |
633 \medskip The next example includes an option to show the type of all |
634 \verb,show_types, flag. The antiquotation |
634 variables. The antiquotation |
635 \texttt{{\at}}\verb,{term [show_types] "%x y. x"}, produces the |
635 \texttt{{\at}}\verb,{term [show_types] "%x y. x"}, produces the |
636 output @{term [show_types] "%x y. x"}. Type inference has figured |
636 output @{term [show_types] "%x y. x"}. Type inference has figured |
637 out the most general typings in the present theory context. Terms |
637 out the most general typings in the present theory context. Terms |
638 may acquire different typings due to constraints imposed by their |
638 may acquire different typings due to constraints imposed by their |
639 environment; within a proof, for example, variables are given the |
639 environment; within a proof, for example, variables are given the |