NEWS
 changeset 46752 e9e7209eb375 parent 46732 ac701d7f7c3b child 46834 a5fa1dc55945
equal inserted replaced
46751:6b94c39b7366 46752:e9e7209eb375
`    88 predicate and what a set.  It can be helpful to carry out that step in`
`    88 predicate and what a set.  It can be helpful to carry out that step in`
`    89 Isabelle2011-1 before jumping right into the current release.`
`    89 Isabelle2011-1 before jumping right into the current release.`
`    90 `
`    90 `
`    91 * New type synonym 'a rel = ('a * 'a) set`
`    91 * New type synonym 'a rel = ('a * 'a) set`
`    92 `
`    92 `
`       `
`    93 * More default pred/set conversions on a couple of relation operations`
`       `
`    94 and predicates.  Consolidation of some relation theorems:`
`       `
`    95 `
`       `
`    96   converse_def ~> converse_unfold`
`       `
`    97   rel_comp_def ~> rel_comp_unfold`
`       `
`    98   symp_def ~> (dropped, use symp_def and sym_def instead)`
`       `
`    99   transp_def ~> transp_trans`
`       `
`   100   Domain_def ~> Domain_unfold`
`       `
`   101   Range_def ~> Domain_converse [symmetric]`
`       `
`   102 `
`       `
`   103 INCOMPATIBILITY.`
`       `
`   104 `
`    93 * Consolidated various theorem names relating to Finite_Set.fold`
`   105 * Consolidated various theorem names relating to Finite_Set.fold`
`    94 combinator:`
`   106 combinator:`
`    95 `
`   107 `
`    96   inf_INFI_fold_inf ~> inf_INF_fold_inf`
`   108   inf_INFI_fold_inf ~> inf_INF_fold_inf`
`    97   sup_SUPR_fold_sup ~> sup_SUP_fold_sup`
`   109   sup_SUPR_fold_sup ~> sup_SUP_fold_sup`
`    98   INFI_fold_inf ~> INF_fold_inf`
`   110   INFI_fold_inf ~> INF_fold_inf`
`    99   SUPR_fold_sup ~> SUP_fold_sup`
`   111   SUPR_fold_sup ~> SUP_fold_sup`
`   100   union_set ~> union_set_fold`
`   112   union_set ~> union_set_fold`
`   101   minus_set ~> minus_set_fold`
`   113   minus_set ~> minus_set_fold`
`   102   `
`   114 `
`   103 INCOMPATIBILITY.`
`   115 INCOMPATIBILITY.`
`   104 `
`   116 `
`   105 * Consolidated theorem names concerning fold combinators:`
`   117 * Consolidated theorem names concerning fold combinators:`
`   106 `
`   118 `
`   107   INFI_set_fold ~> INF_set_fold`
`   119   INFI_set_fold ~> INF_set_fold`