2000-06-21 paulson new theorems lepoll_Ord_imp_eqpoll, lesspoll_imp_eqpoll, lesspoll_nat_is_Finite
2000-06-21 paulson new theorem UN_empty; it and Un_empty inserted by AddIffs
2000-06-21 paulson generalized {Domain,Range}_partial_func to {Domain,Range}_Collect_split
2000-06-21 paulson tidied; weakened the (impossible) premises of setsum_UN_disjoint
2000-06-20 paulson new module for heaps
2000-06-20 paulson now uses the heap data structure for BEST_FIRST
2000-06-20 paulson new file heap.ML
2000-06-20 paulson changed the Schubert Steamroller proof
2000-06-20 paulson another brick in the wall
2000-06-20 paulson changed a step for the improved rules for setsum
2000-06-20 paulson deleted a step made redundant by the improved rules for setsum
2000-06-20 paulson replaced the useless [p]subset_insertD by [p]subset_insert_iff
2000-06-20 paulson now setsum f A = 0 unless A is finite
2000-06-20 paulson now setsum f A = 0 unless A is finite; proved setsum_cong
2000-06-16 paulson real simprocs
2000-06-16 paulson fixed for removal of subset_empty
2000-06-16 paulson this proof needs more detail
2000-06-16 paulson uncommented the last 2 examples; tidied
2000-06-16 paulson new lemma real_minus_diff_eq
2000-06-16 paulson fixed the installation of linear arithmetic for the reals
2000-06-16 paulson some missing simprules for integer linear arithmetic
2000-06-16 paulson tidied for new card_seteq
2000-06-16 paulson subset_empty is no longer a simprule
2000-06-16 paulson renamed psubset_card -> psubset_card_mono
2000-06-16 paulson Finally "AddEs [equalityE]" is IN and "AddDs [equals0D, sym RS equals0D]" is OUT
2000-06-16 paulson inserted some "addsimps [subset_empty]"; also tidied (a lot)
2000-06-16 paulson tracing flag for arith_tac
2000-06-15 berghofe Now also proves monotonicity when in quick_and_dirty mode.
Loading...
(0) -3000 -1000 -300 -100 -50 -28 +28 +50 +100 +300 +1000 +3000 +10000 +30000 tip