NEWS
changeset 57251 f51985ebd152
parent 57246 62746a41cc0c
child 57252 19b7ace1c5da
equal deleted inserted replaced
57250:cddaf5b93728 57251:f51985ebd152
   363     filter_rel ~> rel_filter
   363     filter_rel ~> rel_filter
   364     fset_rel ~> rel_fset (in "Library/FSet.thy")
   364     fset_rel ~> rel_fset (in "Library/FSet.thy")
   365     cset_rel ~> rel_cset (in "Library/Countable_Set_Type.thy")
   365     cset_rel ~> rel_cset (in "Library/Countable_Set_Type.thy")
   366     vset ~> rel_vset (in "Library/Quotient_Set.thy")
   366     vset ~> rel_vset (in "Library/Quotient_Set.thy")
   367 
   367 
   368 * New theory:
   368 * New theories:
   369     Cardinals/Ordinal_Arithmetic.thy
   369     Cardinals/Ordinal_Arithmetic.thy
       
   370     Library/Tree
   370 
   371 
   371 * Theory reorganizations:
   372 * Theory reorganizations:
   372   * Big_Operators.thy ~> Groups_Big.thy and Lattices_Big.thy
   373   * Big_Operators.thy ~> Groups_Big.thy and Lattices_Big.thy
   373 
   374 
   374 * New internal SAT solver "cdclite" that produces models and proof traces.
   375 * New internal SAT solver "cdclite" that produces models and proof traces.