equal
deleted
inserted
replaced
70 pruned from any tinkering with former theorems mem_def and |
70 pruned from any tinkering with former theorems mem_def and |
71 Collect_def. For developments which deliberately mixed predicates and |
71 Collect_def. For developments which deliberately mixed predicates and |
72 sets, a planning step is necessary to determine what should become a |
72 sets, a planning step is necessary to determine what should become a |
73 predicate and what a set. It can be helpful to carry out that step in |
73 predicate and what a set. It can be helpful to carry out that step in |
74 Isabelle2011-1 before jumping right into the current release. |
74 Isabelle2011-1 before jumping right into the current release. |
|
75 |
|
76 * New type synonym 'a rel = ('a * 'a) set |
75 |
77 |
76 * Consolidated various theorem names relating to Finite_Set.fold |
78 * Consolidated various theorem names relating to Finite_Set.fold |
77 combinator: |
79 combinator: |
78 |
80 |
79 inf_INFI_fold_inf ~> inf_INF_fold_inf |
81 inf_INFI_fold_inf ~> inf_INF_fold_inf |