equal
deleted
inserted
replaced
132 |
132 |
133 fun level_of_type_sys Many_Typed = All_Types |
133 fun level_of_type_sys Many_Typed = All_Types |
134 | level_of_type_sys (Preds (_, level)) = level |
134 | level_of_type_sys (Preds (_, level)) = level |
135 | level_of_type_sys (Tags (_, level)) = level |
135 | level_of_type_sys (Tags (_, level)) = level |
136 |
136 |
137 val is_type_level_virtually_sound = |
137 fun is_type_level_virtually_sound s = |
138 member (op =) [All_Types, Nonmonotonic_Types] |
138 s = All_Types orelse s = Nonmonotonic_Types |
139 val is_type_sys_virtually_sound = |
139 val is_type_sys_virtually_sound = |
140 is_type_level_virtually_sound o level_of_type_sys |
140 is_type_level_virtually_sound o level_of_type_sys |
141 |
141 |
142 fun is_type_level_fairly_sound level = |
142 fun is_type_level_fairly_sound level = |
143 is_type_level_virtually_sound level orelse level = Finite_Types |
143 is_type_level_virtually_sound level orelse level = Finite_Types |