equal
deleted
inserted
replaced
21 |
21 |
22 (* data administration *) |
22 (* data administration *) |
23 |
23 |
24 val direction_of = Thm.dest_binop o Thm.dest_arg o cprop_of; |
24 val direction_of = Thm.dest_binop o Thm.dest_arg o cprop_of; |
25 |
25 |
|
26 val transfer_morphism_key = Drule.strip_imp_concl (Thm.cprop_of @{thm transfer_morphismI}); |
|
27 |
26 fun check_morphism_key ctxt key = |
28 fun check_morphism_key ctxt key = |
27 let |
29 let |
28 val _ = (Thm.match o pairself Thm.cprop_of) (@{thm transfer_morphismI}, key) |
30 val _ = Thm.match (transfer_morphism_key, Thm.cprop_of key) |
29 handle Pattern.MATCH => error |
31 handle Pattern.MATCH => error ("Transfer: expected theorem of the form " |
30 ("Transfer: expected theorem of the form " ^ quote (Display.string_of_thm ctxt @{thm transfer_morphismI})); |
32 ^ quote (Syntax.string_of_term ctxt (Thm.term_of transfer_morphism_key))); |
31 in direction_of key end; |
33 in direction_of key end; |
32 |
34 |
33 type entry = { inj : thm list, embed : thm list, return : thm list, cong : thm list, |
35 type entry = { inj : thm list, embed : thm list, return : thm list, cong : thm list, |
34 hints : string list }; |
36 hints : string list }; |
35 |
37 |