equal
deleted
inserted
replaced
175 |
175 |
176 fun gen_pcpodef_proof prep_term pcpo ((def, name), typ, set, opt_morphs) thy = |
176 fun gen_pcpodef_proof prep_term pcpo ((def, name), typ, set, opt_morphs) thy = |
177 let |
177 let |
178 val (goal, att) = |
178 val (goal, att) = |
179 gen_prepare_pcpodef prep_term pcpo def name typ set opt_morphs thy; |
179 gen_prepare_pcpodef prep_term pcpo def name typ set opt_morphs thy; |
180 in IsarThy.theorem_i PureThy.internalK ("", [att]) (goal, ([], [])) thy end; |
180 in IsarThy.theorem_i PureThy.internalK ("", [att]) (goal, []) thy end; |
181 |
181 |
182 fun pcpodef_proof x = gen_pcpodef_proof read_term true x; |
182 fun pcpodef_proof x = gen_pcpodef_proof read_term true x; |
183 fun pcpodef_proof_i x = gen_pcpodef_proof cert_term true x; |
183 fun pcpodef_proof_i x = gen_pcpodef_proof cert_term true x; |
184 |
184 |
185 fun cpodef_proof x = gen_pcpodef_proof read_term false x; |
185 fun cpodef_proof x = gen_pcpodef_proof read_term false x; |