| Sun, 24 Nov 2013 13:06:22 +0000 |
paulson |
cleaned up some messy proofs
|
changeset |
files
|
| Sun, 24 Nov 2013 13:34:23 +0100 |
nipkow |
tuned
|
changeset |
files
|
| Sun, 24 Nov 2013 13:22:59 +0100 |
nipkow |
replaced bad example
|
changeset |
files
|
| Sun, 24 Nov 2013 00:31:50 +0000 |
paulson |
polished some ancient proofs
|
changeset |
files
|
| Sat, 23 Nov 2013 16:41:37 +0000 |
paulson |
merged
|
changeset |
files
|
| Sat, 23 Nov 2013 16:39:48 +0000 |
paulson |
Simplified, tidied and generalised proofs esp of Binomial Theorem.
|
changeset |
files
|
| Sat, 23 Nov 2013 17:15:44 +0100 |
wenzelm |
more uniform / rigid checking of Goal.prove_common vs. Proof.conclude_goal -- NB: Goal.prove_common cannot check hyps right now, e.g. due to undeclared Simplifier prems;
|
changeset |
files
|
| Sat, 23 Nov 2013 17:07:36 +0100 |
wenzelm |
more accurate goal context;
|
changeset |
files
|
| Sat, 23 Nov 2013 17:07:11 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 23 Nov 2013 16:39:08 +0100 |
wenzelm |
more accurate goal context;
|
changeset |
files
|
| Sat, 23 Nov 2013 13:11:12 +0100 |
wenzelm |
more official option;
|
changeset |
files
|
| Fri, 22 Nov 2013 21:13:44 +0100 |
wenzelm |
clarified node edits sent to prover -- Clear/Blob only required for text edits within editor;
|
changeset |
files
|