equal
deleted
inserted
replaced
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. |