chiark
/
gitweb
/
~ian
/
topbloke-formulae.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
| inline |
side by side
(from parent 1:
c39f3f1
)
wip dependency insertion
author
Ian Jackson
<ijackson@chiark.greenend.org.uk>
Wed, 14 Mar 2012 23:22:20 +0000
(23:22 +0000)
committer
Ian Jackson
<ijackson@chiark.greenend.org.uk>
Wed, 14 Mar 2012 23:22:20 +0000
(23:22 +0000)
article.tex
patch
|
blob
|
history
diff --git
a/article.tex
b/article.tex
index 7ec582e666ef94e6b55ba1e682e1866a1048cb03..0ed90a67314921007898565e28874630769e8908 100644
(file)
--- a/
article.tex
+++ b/
article.tex
@@
-855,7
+855,6
@@
$$
\p \neq \pr \land L \nothaspatch \p : & C \nothaspatch \p
\end{cases}
$$
-
\proofstarts
~ Consider some $D \in \py$.
$D \neq C$ so $D \le C \equiv D \le L \lor D \le R^+$.