equal
deleted
inserted
replaced
171 val (goal, pcpodef_result) = |
171 val (goal, pcpodef_result) = |
172 prepare_pcpodef prep_term pcpo def name typ set opt_morphs thy; |
172 prepare_pcpodef prep_term pcpo def name typ set opt_morphs thy; |
173 fun after_qed [[th]] = ProofContext.theory (pcpodef_result th); |
173 fun after_qed [[th]] = ProofContext.theory (pcpodef_result th); |
174 in Proof.theorem_i NONE after_qed [[(goal, [])]] (ProofContext.init thy) end; |
174 in Proof.theorem_i NONE after_qed [[(goal, [])]] (ProofContext.init thy) end; |
175 |
175 |
176 fun pcpodef_proof x = gen_pcpodef_proof ProofContext.read_term true x; |
176 fun pcpodef_proof x = gen_pcpodef_proof Syntax.read_term true x; |
177 fun pcpodef_proof_i x = gen_pcpodef_proof ProofContext.cert_term true x; |
177 fun pcpodef_proof_i x = gen_pcpodef_proof Syntax.check_term true x; |
178 |
178 |
179 fun cpodef_proof x = gen_pcpodef_proof ProofContext.read_term false x; |
179 fun cpodef_proof x = gen_pcpodef_proof Syntax.read_term false x; |
180 fun cpodef_proof_i x = gen_pcpodef_proof ProofContext.cert_term false x; |
180 fun cpodef_proof_i x = gen_pcpodef_proof Syntax.check_term false x; |
181 |
181 |
182 |
182 |
183 (** outer syntax **) |
183 (** outer syntax **) |
184 |
184 |
185 local structure P = OuterParse and K = OuterKeyword in |
185 local structure P = OuterParse and K = OuterKeyword in |