equal
deleted
inserted
replaced
1 theory Ind_Code |
1 theory Ind_Code |
2 imports Ind_General_Scheme "../FirstSteps" |
2 imports Ind_General_Scheme "../First_Steps" |
3 begin |
3 begin |
4 |
4 |
5 section {* The Gory Details\label{sec:code} *} |
5 section {* The Gory Details\label{sec:code} *} |
6 |
6 |
7 text {* |
7 text {* |
90 |
90 |
91 local_setup %gray {* fn lthy => |
91 local_setup %gray {* fn lthy => |
92 let |
92 let |
93 val def = defn_aux lthy eo_orules eo_preds (e_pred, e_arg_tys) |
93 val def = defn_aux lthy eo_orules eo_preds (e_pred, e_arg_tys) |
94 in |
94 in |
95 tracing (string_of_term lthy def); lthy |
95 pwriteln (pretty_term lthy def); lthy |
96 end *} |
96 end *} |
97 |
97 |
98 text {* |
98 text {* |
99 where we use the shorthands defined in Figure~\ref{fig:shorthands}. |
99 where we use the shorthands defined in Figure~\ref{fig:shorthands}. |
100 The testcase calls @{ML defn_aux} for the predicate @{text "even"} and prints |
100 The testcase calls @{ML defn_aux} for the predicate @{text "even"} and prints |
110 local_setup %gray {* fn lthy => |
110 local_setup %gray {* fn lthy => |
111 let |
111 let |
112 val arg = (fresh_pred, fresh_arg_tys) |
112 val arg = (fresh_pred, fresh_arg_tys) |
113 val def = defn_aux lthy fresh_orules [fresh_pred] arg |
113 val def = defn_aux lthy fresh_orules [fresh_pred] arg |
114 in |
114 in |
115 tracing (string_of_term lthy def); lthy |
115 pwriteln (pretty_term lthy def); lthy |
116 end *} |
116 end *} |
117 |
117 |
118 |
118 |
119 text {* |
119 text {* |
120 we obtain |
120 we obtain |
594 Pretty.big_list "Params2 from the predicate:" (map (pretty_cterm ctxt) params2), |
594 Pretty.big_list "Params2 from the predicate:" (map (pretty_cterm ctxt) params2), |
595 Pretty.big_list "Prems1 from the rule:" (map (pretty_thm ctxt) prems1), |
595 Pretty.big_list "Prems1 from the rule:" (map (pretty_thm ctxt) prems1), |
596 Pretty.big_list "Prems2 from the predicate:" (map (pretty_thm ctxt) prems2)] |
596 Pretty.big_list "Prems2 from the predicate:" (map (pretty_thm ctxt) prems2)] |
597 in |
597 in |
598 pps |> Pretty.chunks |
598 pps |> Pretty.chunks |
599 |> tracing o Pretty.string_of |
599 |> pwriteln |
600 end*} |
600 end*} |
601 text_raw{* |
601 text_raw{* |
602 \end{isabelle} |
602 \end{isabelle} |
603 \end{minipage} |
603 \end{minipage} |
604 \caption{A helper function that prints out the parameters and premises that |
604 \caption{A helper function that prints out the parameters and premises that |