Thu, 25 Apr 2013 08:56:37 +0200 no eta-expansion for case in split rules and case_conv
blanchet [Thu, 25 Apr 2013 08:56:37 +0200] rev 51770
no eta-expansion for case in split rules and case_conv
Thu, 25 Apr 2013 08:56:10 +0200 simplified code -- no need for two attempts, the error we get from mixfix the first time is good (and better to get than a parse error in the specification because the user tries to use a mixfix that silently failed)
blanchet [Thu, 25 Apr 2013 08:56:10 +0200] rev 51769
simplified code -- no need for two attempts, the error we get from mixfix the first time is good (and better to get than a parse error in the specification because the user tries to use a mixfix that silently failed)
Wed, 24 Apr 2013 22:48:22 +0200 proper error generated for wrong mixfix
blanchet [Wed, 24 Apr 2013 22:48:22 +0200] rev 51768
proper error generated for wrong mixfix
Wed, 24 Apr 2013 18:49:52 +0200 honor user-specified name for relator + generalize syntax
blanchet [Wed, 24 Apr 2013 18:49:52 +0200] rev 51767
honor user-specified name for relator + generalize syntax
Wed, 24 Apr 2013 17:47:22 +0200 renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
blanchet [Wed, 24 Apr 2013 17:47:22 +0200] rev 51766
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
Wed, 24 Apr 2013 17:03:43 +0200 added "fundef_cong" attribute to "map_cong"
blanchet [Wed, 24 Apr 2013 17:03:43 +0200] rev 51765
added "fundef_cong" attribute to "map_cong"
Wed, 24 Apr 2013 16:43:19 +0200 optimized proofs
traytel [Wed, 24 Apr 2013 16:43:19 +0200] rev 51764
optimized proofs
Wed, 24 Apr 2013 16:21:23 +0200 apply arguments to f and g in "case_cong"
blanchet [Wed, 24 Apr 2013 16:21:23 +0200] rev 51763
apply arguments to f and g in "case_cong"
Wed, 24 Apr 2013 15:42:00 +0200 derive "map_cong"
blanchet [Wed, 24 Apr 2013 15:42:00 +0200] rev 51762
derive "map_cong"
Wed, 24 Apr 2013 14:15:01 +0200 renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
blanchet [Wed, 24 Apr 2013 14:15:01 +0200] rev 51761
renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 tip