equal
deleted
inserted
replaced
149 val [x, c] = [("x", ty), ("c", ty --> @{typ bool})] |
149 val [x, c] = [("x", ty), ("c", ty --> @{typ bool})] |
150 |> Variable.variant_frees lthy [rel] |
150 |> Variable.variant_frees lthy [rel] |
151 |> map Free |
151 |> map Free |
152 in |
152 in |
153 lambda c |
153 lambda c |
154 (HOLogic.mk_exists |
154 (HOLogic.exists_const ty $ |
155 ("x", ty, HOLogic.mk_eq (c, (rel $ x)))) |
155 lambda x (HOLogic.mk_eq (c, (rel $ x)))) |
156 end |
156 end |
157 *} |
157 *} |
|
158 |
|
159 |
|
160 ML {* |
|
161 typedef_term @{term "x::nat\<Rightarrow>nat\<Rightarrow>bool"} @{typ nat} @{context} |
|
162 |> Syntax.string_of_term @{context} |
|
163 |> writeln |
|
164 *} |
|
165 |
158 |
166 |
159 ML {* |
167 ML {* |
160 (* makes the new type definitions and proves non-emptyness*) |
168 (* makes the new type definitions and proves non-emptyness*) |
161 fun typedef_make (qty_name, rel, ty) lthy = |
169 fun typedef_make (qty_name, rel, ty) lthy = |
162 let |
170 let |