equal
deleted
inserted
replaced
1 (* Title: HOL/hologic.ML |
1 (* Title: HOL/hologic.ML |
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson and Markus Wenzel |
2 Author: Lawrence C Paulson and Markus Wenzel |
4 |
3 |
5 Abstract syntax operations for HOL. |
4 Abstract syntax operations for HOL. |
6 *) |
5 *) |
7 |
6 |
142 | dest_setT T = raise TYPE ("dest_setT: set type expected", [T], []); |
141 | dest_setT T = raise TYPE ("dest_setT: set type expected", [T], []); |
143 |
142 |
144 fun mk_set T ts = |
143 fun mk_set T ts = |
145 let |
144 let |
146 val sT = mk_setT T; |
145 val sT = mk_setT T; |
147 val empty = Const ("Orderings.bot", sT); |
146 val empty = Const ("Set.empty", sT); |
148 fun insert t u = Const ("insert", T --> sT --> sT) $ t $ u; |
147 fun insert t u = Const ("insert", T --> sT --> sT) $ t $ u; |
149 in fold_rev insert ts empty end; |
148 in fold_rev insert ts empty end; |
150 |
149 |
151 fun mk_UNIV T = Const ("Set.UNIV", mk_setT T); |
150 fun mk_UNIV T = Const ("Set.UNIV", mk_setT T); |
152 |
151 |