equal
deleted
inserted
replaced
14 |
14 |
15 * HOL: Removed the obsolete syntax "Compl A"; use -A for set |
15 * HOL: Removed the obsolete syntax "Compl A"; use -A for set |
16 complement; |
16 complement; |
17 |
17 |
18 * HOL: the predicate "inj" is now defined by translation to "inj_on"; |
18 * HOL: the predicate "inj" is now defined by translation to "inj_on"; |
|
19 |
|
20 * HOL/datatype: mutual_induct_tac no longer exists -- |
|
21 use induct_tac "x_1 ... x_n" instead of mutual_induct_tac ["x_1", ..., "x_n"] |
19 |
22 |
20 * HOL/typedef: fixed type inference for representing set; type |
23 * HOL/typedef: fixed type inference for representing set; type |
21 arguments now have to occur explicitly on the rhs as type constraints; |
24 arguments now have to occur explicitly on the rhs as type constraints; |
22 |
25 |
23 * ZF: The con_defs part of an inductive definition may no longer refer |
26 * ZF: The con_defs part of an inductive definition may no longer refer |