equal
deleted
inserted
replaced
357 |
357 |
358 (* prove isomorphism properties *) |
358 (* prove isomorphism properties *) |
359 |
359 |
360 fun mk_funs_inv thm = |
360 fun mk_funs_inv thm = |
361 let |
361 let |
362 val {thy, prop, ...} = rep_thm thm; |
362 val thy = Thm.theory_of_thm thm; |
|
363 val prop = Thm.prop_of thm; |
363 val _ $ (_ $ ((S as Const (_, Type (_, [U, _]))) $ _ )) $ |
364 val _ $ (_ $ ((S as Const (_, Type (_, [U, _]))) $ _ )) $ |
364 (_ $ (_ $ (r $ (a $ _)) $ _)) = Type.freeze prop; |
365 (_ $ (_ $ (r $ (a $ _)) $ _)) = Type.freeze prop; |
365 val used = add_term_tfree_names (a, []); |
366 val used = add_term_tfree_names (a, []); |
366 |
367 |
367 fun mk_thm i = |
368 fun mk_thm i = |