changeset 15979 | c81578ac2d31 |
parent 15705 | b5edb9dcec9a |
child 17065 | c1cd17010a1b |
15978:f044579b147c | 15979:c81578ac2d31 |
---|---|
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 |