equal
deleted
inserted
replaced
298 |> fst |
298 |> fst |
299 |> Syntax.string_of_term @{context} |
299 |> Syntax.string_of_term @{context} |
300 |> writeln |
300 |> writeln |
301 *} |
301 *} |
302 |
302 |
303 (* |
303 ML {* op --> *} |
|
304 ML {* op ---> *} |
|
305 term FUN_REL |
|
306 term LIST_REL |
|
307 |
|
308 ML {* @{const_name "op ="} *} |
304 ML {* |
309 ML {* |
305 fun tyRel ty rty rel lthy = |
310 fun tyRel ty rty rel lthy = |
306 if ty = rty |
311 if ty = rty then rel |
307 then rel |
|
308 else (case ty of |
312 else (case ty of |
309 Type (s, tys) => |
313 Type (s, tys) => |
|
314 let |
|
315 val tys_rel = map (fn ty => ty --> ty --> @{typ bool}) tys; |
|
316 val ty_out = ty --> ty --> @{typ bool}; |
|
317 val tys_out = tys_rel ---> ty_out; |
|
318 in |
310 (case (lookup (ProofContext.theory_of lthy) s) of |
319 (case (lookup (ProofContext.theory_of lthy) s) of |
311 SOME (info) => list_comb (Const (#relfun info, ?????), map (tyRel ???) tys) |
320 SOME (info) => list_comb (Const (#relfun info, tys_out), map (fn ty => tyRel ty rty rel lthy) tys) |
312 NONE => (op =):: tys |
321 | NONE => Const (@{const_name "op ="}, ty --> ty --> @{typ bool}) |
313 ) |
322 ) |
314 | _ => (op =):: ty) |
323 end |
315 *} |
324 | _ => Const (@{const_name "op ="}, ty --> ty --> @{typ bool})) |
316 |
325 *} |
317 ML {* |
326 |
|
327 ML {* |
|
328 cterm_of @{theory} (tyRel @{typ "trm \<Rightarrow> bool"} @{typ "trm"} @{term "RR"} @{context}) |
|
329 *} |
|
330 |
|
331 (* ML {* |
318 |
332 |
319 fun regularise trm \<Rightarrow> new_trm |
333 fun regularise trm \<Rightarrow> new_trm |
320 (case trm of |
334 (case trm of |
321 ?? |
335 ?? |
322 ) |
336 ) |