26 -- "now uniform 'a::bar instead of default sort for first occurence (!)" |
26 -- "now uniform 'a::bar instead of default sort for first occurence (!)" |
27 |
27 |
28 |
28 |
29 |
29 |
30 *** HOL *** |
30 *** HOL *** |
|
31 |
|
32 * Session HOL-Word: Discontinued many redundant theorems specific to type |
|
33 'a word. INCOMPATIBILITY, use the corresponding generic theorems instead. |
|
34 |
|
35 word_sub_alt ~> word_sub_wi |
|
36 word_add_alt ~> word_add_def |
|
37 word_mult_alt ~> word_mult_def |
|
38 word_minus_alt ~> word_minus_def |
|
39 word_0_alt ~> word_0_wi |
|
40 word_1_alt ~> word_1_wi |
|
41 word_add_0 ~> add_0_left |
|
42 word_add_0_right ~> add_0_right |
|
43 word_mult_1 ~> mult_1_left |
|
44 word_mult_1_right ~> mult_1_right |
|
45 word_add_commute ~> add_commute |
|
46 word_add_assoc ~> add_assoc |
|
47 word_add_left_commute ~> add_left_commute |
|
48 word_mult_commute ~> mult_commute |
|
49 word_mult_assoc ~> mult_assoc |
|
50 word_mult_left_commute ~> mult_left_commute |
|
51 word_left_distrib ~> left_distrib |
|
52 word_right_distrib ~> right_distrib |
|
53 word_left_minus ~> left_minus |
|
54 word_diff_0_right ~> diff_0_right |
|
55 word_diff_self ~> diff_self |
|
56 word_add_ac ~> add_ac |
|
57 word_mult_ac ~> mult_ac |
|
58 word_plus_ac0 ~> add_0_left add_0_right add_ac |
|
59 word_times_ac1 ~> mult_1_left mult_1_right mult_ac |
31 |
60 |
32 * Clarified attribute "mono_set": pure declararation without modifying |
61 * Clarified attribute "mono_set": pure declararation without modifying |
33 the result of the fact expression. |
62 the result of the fact expression. |
34 |
63 |
35 * "Transitive_Closure.ntrancl": bounded transitive closure on |
64 * "Transitive_Closure.ntrancl": bounded transitive closure on |