equal
deleted
inserted
replaced
598 val o_def = @{thm o_def} |
598 val o_def = @{thm o_def} |
599 val injD = @{thm injD} |
599 val injD = @{thm injD} |
600 val datatype_injI = @{thm datatype_injI} |
600 val datatype_injI = @{thm datatype_injI} |
601 val range_ex1_eq = @{thm range_ex1_eq} |
601 val range_ex1_eq = @{thm range_ex1_eq} |
602 val expand_fun_eq = @{thm expand_fun_eq} |
602 val expand_fun_eq = @{thm expand_fun_eq} |
|
603 val sup_fun_eq = @{thm sup_fun_eq} |
|
604 val sup_bool_eq = @{thm sup_bool_eq} |
603 *} |
605 *} |
604 |
606 |
605 end |
607 end |