equal
deleted
inserted
replaced
1244 \begin{figure}[t] |
1244 \begin{figure}[t] |
1245 \begin{minipage}{\textwidth} |
1245 \begin{minipage}{\textwidth} |
1246 \begin{isabelle}*} |
1246 \begin{isabelle}*} |
1247 ML{*fun print_ss ctxt ss = |
1247 ML{*fun print_ss ctxt ss = |
1248 let |
1248 let |
1249 val {simps, congs, procs, ...} = Simplifier.dest_ss ss |
1249 val {simps, congs, procs, ...} = MetaSimplifier.dest_ss ss |
1250 |
1250 |
1251 fun name_thm (nm, thm) = |
1251 fun name_thm (nm, thm) = |
1252 " " ^ nm ^ ": " ^ (string_of_thm_no_vars ctxt thm) |
1252 " " ^ nm ^ ": " ^ (string_of_thm_no_vars ctxt thm) |
1253 fun name_ctrm (nm, ctrm) = |
1253 fun name_ctrm (nm, ctrm) = |
1254 " " ^ nm ^ ": " ^ (string_of_cterms ctxt ctrm) |
1254 " " ^ nm ^ ": " ^ (string_of_cterms ctxt ctrm) |
1261 |> tracing |
1261 |> tracing |
1262 end*} |
1262 end*} |
1263 text_raw {* |
1263 text_raw {* |
1264 \end{isabelle} |
1264 \end{isabelle} |
1265 \end{minipage} |
1265 \end{minipage} |
1266 \caption{The function @{ML_ind dest_ss in Simplifier} returns a record containing |
1266 \caption{The function @{ML_ind dest_ss in MetaSimplifier} returns a record containing |
1267 all printable information stored in a simpset. We are here only interested in the |
1267 all printable information stored in a simpset. We are here only interested in the |
1268 simplification rules, congruence rules and simprocs.\label{fig:printss}} |
1268 simplification rules, congruence rules and simprocs.\label{fig:printss}} |
1269 \end{figure} *} |
1269 \end{figure} *} |
1270 |
1270 |
1271 |
1271 |