Sat, 28 May 2022 10:45:45 +0200 added lemmas Multiset.{bex_least_element,bex_greatest_element} draft
desharna [Sat, 28 May 2022 10:45:45 +0200] rev 75963
added lemmas Multiset.{bex_least_element,bex_greatest_element}
Fri, 27 May 2022 16:16:45 +0200 added predicate totalp_on and abbreviation totalp
desharna [Fri, 27 May 2022 16:16:45 +0200] rev 75962
added predicate totalp_on and abbreviation totalp
Fri, 27 May 2022 13:46:40 +0200 excluded dummy ATPs from Sledgehammer's default provers
desharna [Fri, 27 May 2022 13:46:40 +0200] rev 75961
excluded dummy ATPs from Sledgehammer's default provers
Wed, 25 May 2022 15:49:12 +0200 redefined order.{,strict_}mono as abbreviations of monotone draft
desharna [Wed, 25 May 2022 15:49:12 +0200] rev 75960
redefined order.{,strict_}mono as abbreviations of monotone
Wed, 25 May 2022 14:39:46 +0200 move monotone from Complete_Partial_Order to Orderings
desharna [Wed, 25 May 2022 14:39:46 +0200] rev 75959
move monotone from Complete_Partial_Order to Orderings
Wed, 25 May 2022 13:06:29 +0200 added lemmas mult{,p}_mono_strong draft
desharna [Wed, 25 May 2022 13:06:29 +0200] rev 75958
added lemmas mult{,p}_mono_strong
Wed, 25 May 2022 10:57:07 +0100 qualified name to fix integrable_cong ambiguity
paulson <lp15@cam.ac.uk> [Wed, 25 May 2022 10:57:07 +0100] rev 75957
qualified name to fix integrable_cong ambiguity
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -7 +7 +10 +30 +100 tip