equal
deleted
inserted
replaced
894 |
894 |
895 section \<open>Tracing methods\<close> |
895 section \<open>Tracing methods\<close> |
896 |
896 |
897 text \<open> |
897 text \<open> |
898 Method tracing is supported by auxiliary print methods provided by @{theory |
898 Method tracing is supported by auxiliary print methods provided by @{theory |
899 Eisbach_Tools}. These include @{method print_fact}, @{method print_term} and |
899 "HOL-Eisbach.Eisbach_Tools"}. These include @{method print_fact}, @{method |
900 @{method print_type}. Whenever a print method is evaluated it leaves the |
900 print_term} and @{method print_type}. Whenever a print method is evaluated |
901 goal unchanged and writes its argument as tracing output. |
901 it leaves the goal unchanged and writes its argument as tracing output. |
902 |
902 |
903 Print methods can be combined with the @{method fail} method to investigate |
903 Print methods can be combined with the @{method fail} method to investigate |
904 the backtracking behaviour of a method. |
904 the backtracking behaviour of a method. |
905 \<close> |
905 \<close> |
906 |
906 |