equal
deleted
inserted
replaced
46 val mk_supports: term -> term -> term |
46 val mk_supports: term -> term -> term |
47 |
47 |
48 val finite_const: typ -> term |
48 val finite_const: typ -> term |
49 val mk_finite_ty: typ -> term -> term |
49 val mk_finite_ty: typ -> term -> term |
50 val mk_finite: term -> term |
50 val mk_finite: term -> term |
51 |
|
52 |
51 |
53 val mk_equiv: thm -> thm |
52 val mk_equiv: thm -> thm |
54 val safe_mk_equiv: thm -> thm |
53 val safe_mk_equiv: thm -> thm |
55 |
54 |
56 val mk_diff: term * term -> term |
55 val mk_diff: term * term -> term |
58 val mk_union: term * term -> term |
57 val mk_union: term * term -> term |
59 val fold_union: term list -> term |
58 val fold_union: term list -> term |
60 val fold_append: term list -> term |
59 val fold_append: term list -> term |
61 val mk_conj: term * term -> term |
60 val mk_conj: term * term -> term |
62 val fold_conj: term list -> term |
61 val fold_conj: term list -> term |
|
62 |
|
63 val to_set: term -> term |
63 |
64 |
64 (* fresh arguments for a term *) |
65 (* fresh arguments for a term *) |
65 val fresh_args: Proof.context -> term -> term list |
66 val fresh_args: Proof.context -> term -> term list |
66 |
67 |
67 (* datatype operations *) |
68 (* datatype operations *) |
181 fun mk_conj (t1, @{term "True"}) = t1 |
182 fun mk_conj (t1, @{term "True"}) = t1 |
182 | mk_conj (@{term "True"}, t2) = t2 |
183 | mk_conj (@{term "True"}, t2) = t2 |
183 | mk_conj (t1, t2) = HOLogic.mk_conj (t1, t2) |
184 | mk_conj (t1, t2) = HOLogic.mk_conj (t1, t2) |
184 |
185 |
185 fun fold_conj trms = fold_rev (curry mk_conj) trms @{term "True"} |
186 fun fold_conj trms = fold_rev (curry mk_conj) trms @{term "True"} |
|
187 |
|
188 |
|
189 (* coerces a list into a set *) |
|
190 fun to_set t = |
|
191 if fastype_of t = @{typ "atom list"} |
|
192 then @{term "set :: atom list => atom set"} $ t |
|
193 else t |
186 |
194 |
187 |
195 |
188 (* produces fresh arguments for a term *) |
196 (* produces fresh arguments for a term *) |
189 |
197 |
190 fun fresh_args ctxt f = |
198 fun fresh_args ctxt f = |