56 Theory_Target.instantiation ([full_tname], [], @{sort at}) thy; |
56 Theory_Target.instantiation ([full_tname], [], @{sort at}) thy; |
57 val ((_, (_, permute_ldef)), lthy) = |
57 val ((_, (_, permute_ldef)), lthy) = |
58 Specification.definition (NONE, ((permute_def_name, []), permute_eqn)) lthy; |
58 Specification.definition (NONE, ((permute_def_name, []), permute_eqn)) lthy; |
59 val ((_, (_, atom_ldef)), lthy) = |
59 val ((_, (_, atom_ldef)), lthy) = |
60 Specification.definition (NONE, ((atom_def_name, []), atom_eqn)) lthy; |
60 Specification.definition (NONE, ((atom_def_name, []), atom_eqn)) lthy; |
61 val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy); |
61 val ctxt_thy = ProofContext.init_global (ProofContext.theory_of lthy); |
62 val permute_def = singleton (ProofContext.export lthy ctxt_thy) permute_ldef; |
62 val permute_def = singleton (ProofContext.export lthy ctxt_thy) permute_ldef; |
63 val atom_def = singleton (ProofContext.export lthy ctxt_thy) atom_ldef; |
63 val atom_def = singleton (ProofContext.export lthy ctxt_thy) atom_ldef; |
64 val class_thm = @{thm at_class} OF [type_definition, atom_def, permute_def]; |
64 val class_thm = @{thm at_class} OF [type_definition, atom_def, permute_def]; |
65 val thy = lthy |
65 val thy = lthy |
66 |> Class.prove_instantiation_instance (K (Tactic.rtac class_thm 1)) |
66 |> Class.prove_instantiation_instance (K (Tactic.rtac class_thm 1)) |