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" |
121 "(([(even, NONE, NoSyn), (odd, NONE, NoSyn)], |
121 "(([(even, NONE, NoSyn), (odd, NONE, NoSyn)], |
122 [((even0,\<dots>), \"\\^E\\^Ftoken\\^Eeven 0\\^E\\^F\\^E\"), |
122 [((even0,\<dots>), \<dots>), |
123 ((evenS,\<dots>), \"\\^E\\^Ftoken\\^Eodd n \<Longrightarrow> even (Suc n)\\^E\\^F\\^E\"), |
123 ((evenS,\<dots>), \<dots>), |
124 ((oddS,\<dots>), \"\\^E\\^Ftoken\\^Eeven n \<Longrightarrow> odd (Suc n)\\^E\\^F\\^E\")]), [])"} |
124 ((oddS,\<dots>), \<dots>)]), [])"} |
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. |