equal
deleted
inserted
replaced
75 le_INFI ~> le_INF_I |
75 le_INFI ~> le_INF_I |
76 INFI_bool_eq ~> INF_bool_eq |
76 INFI_bool_eq ~> INF_bool_eq |
77 SUPR_bool_eq ~> SUP_bool_eq |
77 SUPR_bool_eq ~> SUP_bool_eq |
78 INFI_apply ~> INF_apply |
78 INFI_apply ~> INF_apply |
79 SUPR_apply ~> SUP_apply |
79 SUPR_apply ~> SUP_apply |
|
80 INCOMPATIBILITY. |
|
81 |
|
82 * Theorem collections ball_simps and bex_simps do not contain theorems referring |
|
83 to UNION any longer; these have been moved to collection UN_ball_bex_simps. |
80 INCOMPATIBILITY. |
84 INCOMPATIBILITY. |
81 |
85 |
82 * Archimedian_Field.thy: |
86 * Archimedian_Field.thy: |
83 floor now is defined as parameter of a separate type class floor_ceiling. |
87 floor now is defined as parameter of a separate type class floor_ceiling. |
84 |
88 |