equal
deleted
inserted
replaced
1146 fun name_thm (nm, thm) = |
1146 fun name_thm (nm, thm) = |
1147 " " ^ nm ^ ": " ^ (str_of_thm_no_vars ctxt thm) |
1147 " " ^ nm ^ ": " ^ (str_of_thm_no_vars ctxt thm) |
1148 fun name_ctrm (nm, ctrm) = |
1148 fun name_ctrm (nm, ctrm) = |
1149 " " ^ nm ^ ": " ^ (str_of_cterms ctxt ctrm) |
1149 " " ^ nm ^ ": " ^ (str_of_cterms ctxt ctrm) |
1150 |
1150 |
1151 val s1 = ["Simplification rules:"] |
1151 val s = ["Simplification rules:"] @ (map name_thm simps) @ |
1152 val s2 = map name_thm simps |
1152 ["Congruences rules:"] @ (map name_thm congs) @ |
1153 val s3 = ["Congruences rules:"] |
1153 ["Simproc patterns:"] @ (map name_ctrm procs) |
1154 val s4 = map name_thm congs |
|
1155 val s5 = ["Simproc patterns:"] |
|
1156 val s6 = map name_ctrm procs |
|
1157 in |
1154 in |
1158 (s1 @ s2 @ s3 @ s4 @ s5 @ s6) |
1155 s |> separate "\n" |
1159 |> separate "\n" |
1156 |> implode |
1160 |> implode |
1157 |> warning |
1161 |> warning |
|
1162 end*} |
1158 end*} |
1163 text_raw {* |
1159 text_raw {* |
1164 \end{isabelle} |
1160 \end{isabelle} |
1165 \end{minipage} |
1161 \end{minipage} |
1166 \caption{The function @{ML MetaSimplifier.dest_ss} returns a record containing |
1162 \caption{The function @{ML MetaSimplifier.dest_ss} returns a record containing |