Mercurial > cpdt > repo

comparison src/LogicProg.v @ 327:5cdfbf56afbe

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Cope with coqdoc bug
author Adam Chlipala <adam@chlipala.net>
date Thu, 22 Sep 2011 11:27:33 -0400
parents 5e24554175de
children 386b7ad8849b
comparison
equal deleted inserted replaced
326:f1d390f305d7 327:5cdfbf56afbe
602 %\item%#<li># %\textbf{%#<b>#Uniqueness of Right Inverse#</b>#%}%: [a * b = e -> b = i a]#</li># 602 %\item%#<li># %\textbf{%#<b>#Uniqueness of Right Inverse#</b>#%}%: [a * b = e -> b = i a]#</li>#
603 %\item%#<li># %\textbf{%#<b>#Uniqueness of Left Inverse#</b>#%}%: [a * b = e -> a = i b]#</li># 603 %\item%#<li># %\textbf{%#<b>#Uniqueness of Left Inverse#</b>#%}%: [a * b = e -> a = i b]#</li>#
604 %\item%#<li># %\textbf{%#<b>#Right Cancellation#</b>#%}%: [a * x = b * x -> a = b]#</li># 604 %\item%#<li># %\textbf{%#<b>#Right Cancellation#</b>#%}%: [a * x = b * x -> a = b]#</li>#
605 %\item%#<li># %\textbf{%#<b>#Left Cancellation#</b>#%}%: [x * a = x * b -> a = b]#</li># 605 %\item%#<li># %\textbf{%#<b>#Left Cancellation#</b>#%}%: [x * a = x * b -> a = b]#</li>#
606 %\item%#<li># %\textbf{%#<b>#Distributivity of Inverse#</b>#%}%: [i (a * b) = i b * i a]#</li># 606 %\item%#<li># %\textbf{%#<b>#Distributivity of Inverse#</b>#%}%: [i (a * b) = i b * i a]#</li>#
607 %\item%#<li># %\textbf{%#<b>#Double Inverse#</b>#%}%: [i (i a) = a]#</li># 607 %\item%#<li># %\textbf{%#<b>#Double Inverse#</b>#%}%: [i (][i a) = a]#</li>#
608 %\item%#<li># %\textbf{%#<b>#Identity Inverse#</b>#%}%: [i e = e]#</li># 608 %\item%#<li># %\textbf{%#<b>#Identity Inverse#</b>#%}%: [i e = e]#</li>#
609 #</ul> </li>#%\end{itemize}% 609 #</ul> </li>#%\end{itemize}%
610 610
611 One more use of tactics is allowed in this problem. The following lemma captures one common pattern of reasoning in algebra proofs: *) 611 One more use of tactics is allowed in this problem. The following lemma captures one common pattern of reasoning in algebra proofs: *)
612 612