changeset 15705 | b5edb9dcec9a |
parent 15703 | 727ef1b8b3ee |
child 15979 | c81578ac2d31 |
15704:93163972dbdc | 15705:b5edb9dcec9a |
---|---|
81 ProofContext.read_typ ProofContext.read_term_liberal Attrib.global_attribute; |
81 ProofContext.read_typ ProofContext.read_term_liberal Attrib.global_attribute; |
82 val add_constdefs_i = gen_constdefs ProofContext.cert_vars_liberal |
82 val add_constdefs_i = gen_constdefs ProofContext.cert_vars_liberal |
83 ProofContext.cert_typ ProofContext.cert_term (K I); |
83 ProofContext.cert_typ ProofContext.cert_term (K I); |
84 |
84 |
85 end; |
85 end; |
86 |