equal
deleted
inserted
replaced
878 \<close> |
878 \<close> |
879 |
879 |
880 setup %gray \<open>term_pat_setup\<close> |
880 setup %gray \<open>term_pat_setup\<close> |
881 |
881 |
882 text \<open> |
882 text \<open> |
883 The parser in Line 2 provides us with a context and a string; this string is |
883 The parser in Line 3 provides us with a context and a string; this string is |
884 transformed into a term using the function @{ML_ind read_term_pattern in |
884 transformed into a term using the function @{ML_ind read_term_pattern in |
885 Proof_Context} (Line 5); the next two lines transform the term into a string |
885 Proof_Context} (Line 6); the next two lines transform the term into a string |
886 so that the ML-system can understand it. (All these functions will be explained |
886 so that the ML-system can understand it. (All these functions will be explained |
887 in more detail in later sections.) An example for this antiquotation is: |
887 in more detail in later sections.) An example for this antiquotation is: |
888 |
888 |
889 @{ML_matchresult [display,gray] |
889 @{ML_matchresult [display,gray] |
890 \<open>@{term_pat "Suc (?x::nat)"}\<close> |
890 \<open>@{term_pat "Suc (?x::nat)"}\<close> |