equal
deleted
inserted
replaced
110 fun mk_union (@{term "{}::atom set"}, @{term "{}::atom set"}) = @{term "{}::atom set"} |
110 fun mk_union (@{term "{}::atom set"}, @{term "{}::atom set"}) = @{term "{}::atom set"} |
111 | mk_union (t1 , @{term "{}::atom set"}) = t1 |
111 | mk_union (t1 , @{term "{}::atom set"}) = t1 |
112 | mk_union (@{term "{}::atom set"}, t2) = t2 |
112 | mk_union (@{term "{}::atom set"}, t2) = t2 |
113 | mk_union (t1, t2) = HOLogic.mk_binop @{const_name "sup"} (t1, t2) |
113 | mk_union (t1, t2) = HOLogic.mk_binop @{const_name "sup"} (t1, t2) |
114 |
114 |
115 fun fold_union trms = fold (curry mk_union) trms @{term "{}::atom set"} |
115 fun fold_union trms = fold_rev (curry mk_union) trms @{term "{}::atom set"} |
116 |
116 |
117 |
117 |
118 |
118 |
119 |
119 |
120 (** datatypes **) |
120 (** datatypes **) |