NEWS
changeset 46752 e9e7209eb375
parent 46732 ac701d7f7c3b
child 46834 a5fa1dc55945
equal deleted 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