blanchet [Thu, 25 Apr 2013 08:56:37 +0200] rev 51770
no eta-expansion for case in split rules and case_conv
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)
blanchet [Wed, 24 Apr 2013 22:48:22 +0200] rev 51768
proper error generated for wrong mixfix
blanchet [Wed, 24 Apr 2013 18:49:52 +0200] rev 51767
honor user-specified name for relator + generalize syntax
blanchet [Wed, 24 Apr 2013 17:47:22 +0200] rev 51766
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
blanchet [Wed, 24 Apr 2013 17:03:43 +0200] rev 51765
added "fundef_cong" attribute to "map_cong"
traytel [Wed, 24 Apr 2013 16:43:19 +0200] rev 51764
optimized proofs
blanchet [Wed, 24 Apr 2013 16:21:23 +0200] rev 51763
apply arguments to f and g in "case_cong"
blanchet [Wed, 24 Apr 2013 15:42:00 +0200] rev 51762
derive "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"