equal
deleted
inserted
replaced
40 * new theory section 'setup'; |
40 * new theory section 'setup'; |
41 |
41 |
42 |
42 |
43 *** HOL *** |
43 *** HOL *** |
44 |
44 |
|
45 * HOL/record: now includes concrete syntax for record terms (still |
|
46 lacks important theorems, like surjective pairing and split); |
|
47 |
45 * new force_tac (and its derivations Force_tac, force): combines |
48 * new force_tac (and its derivations Force_tac, force): combines |
46 rewriting and classical reasoning (and whatever other tools) similarly |
49 rewriting and classical reasoning (and whatever other tools) similarly |
47 to auto_tac, but is aimed to solve the given subgoal totally; |
50 to auto_tac, but is aimed to solve the given subgoal totally; |
48 |
51 |
49 * added option_map_eq_Some to simpset() and claset() |
52 * added option_map_eq_Some to simpset() and claset() |