equal
deleted
inserted
replaced
146 |> TheoryTarget.instantiation ([tyco], vs, @{sort itself}) |
146 |> TheoryTarget.instantiation ([tyco], vs, @{sort itself}) |
147 |> `(fn lthy => Syntax.check_term lthy eq) |
147 |> `(fn lthy => Syntax.check_term lthy eq) |
148 |-> (fn eq => Specification.definition (NONE, (Attrib.no_binding, eq))) |
148 |-> (fn eq => Specification.definition (NONE, (Attrib.no_binding, eq))) |
149 |> snd |
149 |> snd |
150 |> Class.prove_instantiation_instance (K (Class.intro_classes_tac [])) |
150 |> Class.prove_instantiation_instance (K (Class.intro_classes_tac [])) |
151 |> LocalTheory.exit |
151 |> LocalTheory.exit_global |
152 |> ProofContext.theory_of |
|
153 end |
152 end |
154 in TypedefPackage.interpretation add_itself end |
153 in TypedefPackage.interpretation add_itself end |
155 *} |
154 *} |
156 |
155 |
157 instantiation bool :: itself |
156 instantiation bool :: itself |