| Mon, 14 Dec 2009 12:14:12 +0100 |
blanchet |
added "no_assms" option to Refute, and include structured proof assumptions by default;
|
file |
diff |
annotate
|
| Wed, 28 Oct 2009 22:04:57 +0100 |
wenzelm |
back to Proof.raw_goal;
|
file |
diff |
annotate
|
| Fri, 02 Oct 2009 21:41:57 +0200 |
wenzelm |
Refute.refute_goal: canonical goal addresses from 1 (renamed from refute_subgoal to clarify change in semantics);
|
file |
diff |
annotate
|
| Fri, 02 Oct 2009 20:51:32 +0200 |
wenzelm |
misc tuning and simplification;
|
file |
diff |
annotate
|
| Sat, 17 May 2008 15:31:42 +0200 |
wenzelm |
cat_lines;
|
file |
diff |
annotate
|
| Mon, 28 Jan 2008 22:27:20 +0100 |
wenzelm |
removed redundant repeatd scanner combinator;
|
file |
diff |
annotate
|
| Sat, 06 Oct 2007 16:50:04 +0200 |
wenzelm |
simplified interfaces for outer syntax;
|
file |
diff |
annotate
|
| Fri, 19 Jan 2007 21:20:10 +0100 |
webertj |
reformatted to 80 chars/line
|
file |
diff |
annotate
|
| Tue, 06 Sep 2005 16:29:39 +0200 |
webertj |
unnecessary parentheses removed
|
file |
diff |
annotate
|
| Tue, 16 Aug 2005 13:42:26 +0200 |
wenzelm |
OuterKeyword;
|
file |
diff |
annotate
|
| Thu, 03 Mar 2005 12:43:01 +0100 |
skalberg |
Move towards standard functions.
|
file |
diff |
annotate
|
| Wed, 10 Mar 2004 20:31:47 +0100 |
webertj |
*** empty log message ***
|
file |
diff |
annotate
|
| Sat, 10 Jan 2004 13:35:10 +0100 |
webertj |
Adding 'refute' to HOL.
|
file |
diff |
annotate
|