equal
deleted
inserted
replaced
23 and ZF); |
23 and ZF); |
24 |
24 |
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'; |
|
29 |
28 |
30 |
29 *** HOL *** |
31 *** HOL *** |
30 |
32 |
31 * new force_tac (and its derivations Force_tac, force): combines |
33 * new force_tac (and its derivations Force_tac, force): combines |
32 rewriting and classical reasoning (and whatever other tools) similarly |
34 rewriting and classical reasoning (and whatever other tools) similarly |