equal
deleted
inserted
replaced
24 HOLogic.mk_binop @{const_name sup} (a, b)) (rev sets) noatoms; |
24 HOLogic.mk_binop @{const_name sup} (a, b)) (rev sets) noatoms; |
25 *} |
25 *} |
26 |
26 |
27 ML {* |
27 ML {* |
28 fun is_atom thy ty = |
28 fun is_atom thy ty = |
29 Sign.of_sort thy (ty, @{sort at}) |
29 Sign.of_sort thy (ty, @{sort at_base}) |
30 |
30 |
31 fun is_atom_set thy (Type ("fun", [t, @{typ bool}])) = is_atom thy t |
31 fun is_atom_set thy (Type ("fun", [t, @{typ bool}])) = is_atom thy t |
32 | is_atom_set _ _ = false; |
32 | is_atom_set _ _ = false; |
33 |
33 |
34 fun is_atom_fset thy (Type ("FSet.fset", [t])) = is_atom thy t |
34 fun is_atom_fset thy (Type ("FSet.fset", [t])) = is_atom thy t |