58 * Rules and tactics that read instantiations (read_instantiate, |
58 * Rules and tactics that read instantiations (read_instantiate, |
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 |
|
64 * Disposed old term read functions (Sign.read_def_terms, |
|
65 Sign.read_term, Thm.read_def_cterms, Thm.read_cterm etc.). |
|
66 INCOMPATIBILITY, should use regular Syntax.read_term, |
|
67 Syntax.read_term_global etc.; see also OldGoals.read_term as last |
|
68 resort for legacy applications. |
63 |
69 |
64 |
70 |
65 |
71 |
66 New in Isabelle2008 (June 2008) |
72 New in Isabelle2008 (June 2008) |
67 ------------------------------- |
73 ------------------------------- |