| Fri, 17 Mar 2006 14:20:24 +0100 |
haftmann |
added example for operational classes and code generator
|
file |
diff |
annotate
|
| Sat, 11 Mar 2006 16:53:10 +0100 |
wenzelm |
nbe: no_document;
|
file |
diff |
annotate
|
| Mon, 27 Feb 2006 14:34:03 +0100 |
nipkow |
added temp. nbe test
|
file |
diff |
annotate
|
| Thu, 16 Feb 2006 21:11:58 +0100 |
wenzelm |
added ex/Abstract_NAT.thy;
|
file |
diff |
annotate
|
| Sun, 12 Feb 2006 10:42:19 +0100 |
kleing |
* moved ThreeDivides from Isar_examples to better suited HOL/ex
|
file |
diff |
annotate
|
| Sat, 14 Jan 2006 17:14:06 +0100 |
wenzelm |
sane ERROR handling;
|
file |
diff |
annotate
|
| Wed, 14 Dec 2005 22:05:22 +0100 |
webertj |
ex/Sudoku.thy
|
file |
diff |
annotate
|
| Fri, 07 Oct 2005 22:59:21 +0200 |
wenzelm |
removed obsolete ex/Tuple.thy;
|
file |
diff |
annotate
|
| Fri, 23 Sep 2005 22:58:50 +0200 |
webertj |
new sat tactic imports resolution proofs from zChaff
|
file |
diff |
annotate
|
| Tue, 20 Sep 2005 13:56:34 +0200 |
wenzelm |
Chinese Unicode example;
|
file |
diff |
annotate
|
| Sat, 17 Sep 2005 18:11:26 +0200 |
wenzelm |
Hebrew: HTML.with_charset;
|
file |
diff |
annotate
|
| Thu, 15 Sep 2005 17:17:01 +0200 |
wenzelm |
added Hebrew.thy;
|
file |
diff |
annotate
|
| Wed, 14 Sep 2005 17:25:52 +0200 |
chaieb |
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
|
file |
diff |
annotate
|
| Thu, 28 Apr 2005 17:08:08 +0200 |
bauerg |
*** empty log message ***
|
file |
diff |
annotate
|
| Mon, 12 Jul 2004 12:11:46 +0200 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Fri, 16 Apr 2004 20:33:16 +0200 |
nipkow |
Moved ring stuff from ex into Ring_and_Field.
|
file |
diff |
annotate
|
| Fri, 16 Apr 2004 18:09:24 +0200 |
berghofe |
Added theory with examples for quickcheck command.
|
file |
diff |
annotate
|
| Thu, 15 Apr 2004 14:17:45 +0200 |
nipkow |
Added ex/Exceptions.thy
|
file |
diff |
annotate
|
| Mon, 29 Mar 2004 15:35:04 +0200 |
skalberg |
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
|
file |
diff |
annotate
|
| Thu, 25 Mar 2004 05:37:32 +0100 |
kleing |
moved MiniML and AVL to archive of formal proofs
|
file |
diff |
annotate
|
| Thu, 11 Mar 2004 11:24:54 +0100 |
webertj |
Refute_Examples added/fixed
|
file |
diff |
annotate
|
| Wed, 10 Mar 2004 22:39:12 +0100 |
webertj |
added Refute_Examples.thy
|
file |
diff |
annotate
|
| Wed, 22 Oct 2003 10:52:36 +0200 |
paulson |
InductiveInvariant_examples illustrates advanced recursive function definitions
|
file |
diff |
annotate
|
| Wed, 08 Oct 2003 15:57:41 +0200 |
paulson |
Merging of ex/cla.ML and ex/mesontest.ML to ex/Classical.thy
|
file |
diff |
annotate
|
| Tue, 25 Mar 2003 09:50:53 +0100 |
berghofe |
Added examples for Presburger arithmetic.
|
file |
diff |
annotate
|
| Mon, 03 Jun 2002 09:36:30 +0200 |
nipkow |
Added ex/MergeSort
|
file |
diff |
annotate
|
| Tue, 05 Feb 2002 23:18:08 +0100 |
wenzelm |
moved SVC stuff to ex;
|
file |
diff |
annotate
|
| Mon, 10 Dec 2001 15:36:05 +0100 |
berghofe |
Added example file for intuitionistic logic (taken from FOL).
|
file |
diff |
annotate
|
| Tue, 04 Dec 2001 17:59:36 +0100 |
wenzelm |
added Higher_Order_Logic.thy;
|
file |
diff |
annotate
|
| Fri, 23 Nov 2001 19:19:35 +0100 |
wenzelm |
time_use_thy "Locales";
|
file |
diff |
annotate
|