60 Class.instantiation ([full_tname], [], @{sort at}) thy; |
60 Class.instantiation ([full_tname], [], @{sort at}) thy; |
61 val ((_, (_, permute_ldef)), lthy) = |
61 val ((_, (_, permute_ldef)), lthy) = |
62 Specification.definition (NONE, ((permute_def_name, []), permute_eqn)) lthy; |
62 Specification.definition (NONE, ((permute_def_name, []), permute_eqn)) lthy; |
63 val ((_, (_, atom_ldef)), lthy) = |
63 val ((_, (_, atom_ldef)), lthy) = |
64 Specification.definition (NONE, ((atom_def_name, []), atom_eqn)) lthy; |
64 Specification.definition (NONE, ((atom_def_name, []), atom_eqn)) lthy; |
65 val ctxt_thy = ProofContext.init_global (ProofContext.theory_of lthy); |
65 val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy); |
66 val permute_def = singleton (ProofContext.export lthy ctxt_thy) permute_ldef; |
66 val permute_def = singleton (Proof_Context.export lthy ctxt_thy) permute_ldef; |
67 val atom_def = singleton (ProofContext.export lthy ctxt_thy) atom_ldef; |
67 val atom_def = singleton (Proof_Context.export lthy ctxt_thy) atom_ldef; |
68 val class_thm = @{thm at_class} OF [type_definition, atom_def, permute_def]; |
68 val class_thm = @{thm at_class} OF [type_definition, atom_def, permute_def]; |
69 val sort_thm = @{thm at_class_sort} OF [type_definition, atom_def] |
69 val sort_thm = @{thm at_class_sort} OF [type_definition, atom_def] |
70 val thy = lthy |
70 val thy = lthy |
71 |> snd o (Local_Theory.note ((sort_thm_name, [simp_attr]), [sort_thm])) |
71 |> snd o (Local_Theory.note ((sort_thm_name, [simp_attr]), [sort_thm])) |
72 |> Class.prove_instantiation_instance (K (rtac class_thm 1)) |
72 |> Class.prove_instantiation_instance (K (rtac class_thm 1)) |