adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

etanercept: tweak header documentation.

This commit is contained in:
Japheth Lim 2015-12-04 16:18:56 +11:00
parent c5496f869e
commit 4c982bd80b
1 changed files with 2 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
lib/Etanercept.thy
View File

@ -23,7 +23,8 @@ text {*
that exhaustively explores the state space of your proposition.
Usage:
Run the "word_refute" command in a proof.
Run the "word_refute" command in a proof. The proof goal should involve only word
and boolean expressions.
Options:
These are config options which can be set using "declare" or "using".
- word_refute_debug enable verbose debugging output
@ -39,8 +40,6 @@ text {*
with GNU statement expressions, but I'm unsure if it's worth it.
- We currently only support 8-, 16-, 32-, and 64-bit words. It would be straightforward to
support other non-standard widths if required.
- Much of the pattern matching in this theory was generated by a script and is quite verbose. It
could probably be simplified.
The tool is named after etanercept, an ill-advised treatment for primary progressive aphasia, a
condition who's symptoms include an inability to find the right words for things. Amusingly the