equal
deleted
inserted
replaced
115 |
115 |
116 local_setup %gray {* fn lthy => |
116 local_setup %gray {* fn lthy => |
117 let |
117 let |
118 val def = defn_aux lthy eo_orules eo_preds (e_pred, e_arg_tys) |
118 val def = defn_aux lthy eo_orules eo_preds (e_pred, e_arg_tys) |
119 in |
119 in |
120 tracing (Syntax.string_of_term lthy def); lthy |
120 tracing (string_of_term lthy def); lthy |
121 end *} |
121 end *} |
122 |
122 |
123 text {* |
123 text {* |
124 where we use the shorthands defined in Figure~\ref{fig:shorthands}. |
124 where we use the shorthands defined in Figure~\ref{fig:shorthands}. |
125 The testcase calls @{ML defn_aux} for the predicate @{text "even"} and prints |
125 The testcase calls @{ML defn_aux} for the predicate @{text "even"} and prints |
135 local_setup %gray {* fn lthy => |
135 local_setup %gray {* fn lthy => |
136 let |
136 let |
137 val def = defn_aux lthy fresh_orules |
137 val def = defn_aux lthy fresh_orules |
138 [fresh_pred] (fresh_pred, fresh_arg_tys) |
138 [fresh_pred] (fresh_pred, fresh_arg_tys) |
139 in |
139 in |
140 tracing (Syntax.string_of_term lthy def); lthy |
140 tracing (string_of_term lthy def); lthy |
141 end *} |
141 end *} |
142 |
142 |
143 |
143 |
144 text {* |
144 text {* |
145 we obtain |
145 we obtain |