equal
deleted
inserted
replaced
25 * new toplevel commands 'thm' and 'thms' for retrieving theorems from |
25 * new toplevel commands 'thm' and 'thms' for retrieving theorems from |
26 the current theory context; |
26 the current theory context; |
27 |
27 |
28 * new theory section 'nonterminals'; |
28 * new theory section 'nonterminals'; |
29 |
29 |
|
30 * new theory section 'setup'; |
|
31 |
30 |
32 |
31 *** HOL *** |
33 *** HOL *** |
32 |
34 |
33 * new force_tac (and its derivations Force_tac, force): combines |
35 * new force_tac (and its derivations Force_tac, force): combines |
34 rewriting and classical reasoning (and whatever other tools) similarly |
36 rewriting and classical reasoning (and whatever other tools) similarly |