59 res_inst_tac, thin_tac, subgoal_tac etc.) now demand a proper proof |
59 res_inst_tac, thin_tac, subgoal_tac etc.) now demand a proper proof |
60 context, which is required for parsing and type-checking. Moreover, |
60 context, which is required for parsing and type-checking. Moreover, |
61 the variables are specified as plain indexnames, not string encodings |
61 the variables are specified as plain indexnames, not string encodings |
62 thereof. INCOMPATIBILITY. |
62 thereof. INCOMPATIBILITY. |
63 |
63 |
64 * Disposed old term read functions (Sign.read_def_terms, |
64 * Disposed old type and term read functions (Sign.read_def_typ, |
65 Sign.read_term, Thm.read_def_cterms, Thm.read_cterm etc.). |
65 Sign.read_typ, Sign.read_def_terms, Sign.read_term, |
66 INCOMPATIBILITY, should use regular Syntax.read_term, |
66 Thm.read_def_cterms, Thm.read_cterm etc.). INCOMPATIBILITY, should |
|
67 use regular Syntax.read_typ, Syntax.read_term, Syntax.read_typ_global, |
67 Syntax.read_term_global etc.; see also OldGoals.read_term as last |
68 Syntax.read_term_global etc.; see also OldGoals.read_term as last |
68 resort for legacy applications. |
69 resort for legacy applications. |
69 |
70 |
70 |
71 |
71 |
72 |