src/HOL/Tools/Nunchaku/nunchaku_problem.ML
 changeset 66622 0916eb2dbaca parent 66618 048524a4f537 child 66623 8fc868e9e1bf
equal inserted replaced
66621:1eb8e87f7f8b 66622:0916eb2dbaca
`   712 `
`   712 `
`   713 fun str_of_nun_copy_spec {abs_ty, rep_ty, subset, quotient, abs, rep} =`
`   713 fun str_of_nun_copy_spec {abs_ty, rep_ty, subset, quotient, abs, rep} =`
`   714   str_of_ty abs_ty ^ " " ^ nun_assign ^ " " ^ str_of_ty rep_ty ^`
`   714   str_of_ty abs_ty ^ " " ^ nun_assign ^ " " ^ str_of_ty rep_ty ^`
`   715   (case subset of`
`   715   (case subset of`
`   716     NONE => ""`
`   716     NONE => ""`
`   717   | SOME s => if is_triv_subset s then "" else "\n  " ^ nun_subset ^ " " ^ str_of_tm s) ^`
`   717   | SOME s =>`
`       `
`   718     if is_triv_subset s then ""`
`       `
`   719     else "\n  " ^ nun_subset ^ " " ^ nun_parens_if_space (str_of_tm s)) ^`
`   718   (* TODO: use nun_quotient when possible *)`
`   720   (* TODO: use nun_quotient when possible *)`
`   719   (case quotient of`
`   721   (case quotient of`
`   720     NONE => ""`
`   722     NONE => ""`
`   721   | SOME q => "\n  " ^ nun_partial_quotient ^ " " ^ str_of_tm q) ^`
`   723   | SOME q => "\n  " ^ nun_partial_quotient ^ " " ^ str_of_tm q) ^`
`   722   "\n  " ^ nun_abstract ^ " " ^ str_of_tm abs ^ "\n  " ^ nun_concrete ^ " " ^ str_of_tm rep;`
`   724   "\n  " ^ nun_abstract ^ " " ^ str_of_tm abs ^ "\n  " ^ nun_concrete ^ " " ^ str_of_tm rep;`