106 |
106 |
107 If we feed into the parser the string that corresponds to our definition |
107 If we feed into the parser the string that corresponds to our definition |
108 of @{term even} and @{term odd} |
108 of @{term even} and @{term odd} |
109 |
109 |
110 @{ML_matchresult [display,gray] |
110 @{ML_matchresult [display,gray] |
111 "let |
111 \<open>let |
112 val input = filtered_input |
112 val input = filtered_input |
113 (\"even and odd \" ^ |
113 ("even and odd " ^ |
114 \"where \" ^ |
114 "where " ^ |
115 \" even0[intro]: \\\"even 0\\\" \" ^ |
115 " even0[intro]: \"even 0\" " ^ |
116 \"| evenS[intro]: \\\"odd n \<Longrightarrow> even (Suc n)\\\" \" ^ |
116 "| evenS[intro]: \"odd n \<Longrightarrow> even (Suc n)\" " ^ |
117 \"| oddS[intro]: \\\"even n \<Longrightarrow> odd (Suc n)\\\" \") |
117 "| oddS[intro]: \"even n \<Longrightarrow> odd (Suc n)\" ") |
118 in |
118 in |
119 parse spec_parser input |
119 parse spec_parser input |
120 end" |
120 end\<close> |
121 "(([(even, NONE, NoSyn), (odd, NONE, NoSyn)], |
121 \<open>(([(even, NONE, NoSyn), (odd, NONE, NoSyn)], |
122 [((even0,_), _), |
122 [((even0,_), _), |
123 ((evenS,_), _), |
123 ((evenS,_), _), |
124 ((oddS,_), _)]), [])"} |
124 ((oddS,_), _)]), [])\<close>} |
125 |
125 |
126 then we get back the specifications of the predicates (with type and syntax annotations), |
126 then we get back the specifications of the predicates (with type and syntax annotations), |
127 and specifications of the introduction rules. This is all the information we |
127 and specifications of the introduction rules. This is all the information we |
128 need for calling the package and setting up the keyword. The latter is |
128 need for calling the package and setting up the keyword. The latter is |
129 done in Lines 5 to 7 in the code below. |
129 done in Lines 5 to 7 in the code below. |