| Fri, 04 Dec 2020 15:07:47 +0100 |
nipkow |
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
|
file |
diff |
annotate
|
| Tue, 23 Feb 2010 14:11:32 +0100 |
haftmann |
merged
|
file |
diff |
annotate
|
| Tue, 23 Feb 2010 10:11:15 +0100 |
haftmann |
dropped axclass; dropped Id; session theory Hoare.thy
|
file |
diff |
annotate
| base
|
| Thu, 11 Feb 2010 22:19:58 +0100 |
wenzelm |
modernized translations;
|
file |
diff |
annotate
|
| Mon, 08 Feb 2010 21:28:27 +0100 |
wenzelm |
modernized some syntax translations;
|
file |
diff |
annotate
|
| Thu, 23 Jul 2009 18:44:09 +0200 |
wenzelm |
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
|
file |
diff |
annotate
|
| Wed, 22 Jul 2009 14:20:32 +0200 |
haftmann |
set intersection and union now named inter and union
|
file |
diff |
annotate
|
| Mon, 16 Mar 2009 18:24:30 +0100 |
wenzelm |
simplified method setup;
|
file |
diff |
annotate
|
| Fri, 13 Mar 2009 19:58:26 +0100 |
wenzelm |
unified type Proof.method and pervasive METHOD combinators;
|
file |
diff |
annotate
|
| Thu, 05 Mar 2009 08:23:11 +0100 |
haftmann |
set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
|
file |
diff |
annotate
|
| Thu, 02 Oct 2008 14:22:36 +0200 |
wenzelm |
major cleanup of hoare_tac.ML: just one copy for Hoare.thy and HoareAbort.thy (only 1 line different), refrain from inspecting the main goal, proper context;
|
file |
diff |
annotate
|
| Wed, 29 Aug 2007 13:58:00 +0200 |
wenzelm |
added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy);
|
file |
diff |
annotate
|
| Wed, 29 Aug 2007 11:10:28 +0200 |
wenzelm |
removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
|
file |
diff |
annotate
|
| Wed, 29 Nov 2006 15:44:51 +0100 |
wenzelm |
simplified method setup;
|
file |
diff |
annotate
|
| Fri, 07 Oct 2005 22:59:18 +0200 |
wenzelm |
print_translation: does not handle _idtdummy;
|
file |
diff |
annotate
|
| Fri, 17 Jun 2005 16:12:49 +0200 |
haftmann |
migrated theory headers to new format
|
file |
diff |
annotate
|
| Sun, 11 Jul 2004 20:33:22 +0200 |
wenzelm |
local_cla/simpset_of;
|
file |
diff |
annotate
|
| Tue, 11 Mar 2003 15:04:24 +0100 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Sun, 22 Dec 2002 15:02:40 +0100 |
nipkow |
removed some problems with print translations
|
file |
diff |
annotate
|
| Fri, 29 Nov 2002 09:48:28 +0100 |
nipkow |
added a few lemmas
|
file |
diff |
annotate
|
| Wed, 06 Nov 2002 14:01:38 +0100 |
nipkow |
a new pointer example and some syntactic sugar
|
file |
diff |
annotate
|
| Mon, 28 Oct 2002 14:29:51 +0100 |
nipkow |
conversion ML -> thy
|
file |
diff |
annotate
|
| Thu, 27 Sep 2001 22:24:28 +0200 |
wenzelm |
renamed "()" to Unity;
|
file |
diff |
annotate
|
| Fri, 21 Jul 2000 16:35:12 +0200 |
prensani |
Updating of some comments
|
file |
diff |
annotate
|
| Mon, 04 Jan 1999 15:07:47 +0100 |
nipkow |
Version 1.0 of linear nat arithmetic.
|
file |
diff |
annotate
|
| Wed, 14 Oct 1998 15:26:31 +0200 |
nipkow |
New many-sorted version.
|
file |
diff |
annotate
|
| Fri, 25 Sep 1998 14:05:13 +0200 |
paulson |
patched obsolete code
|
file |
diff |
annotate
|
| Fri, 24 Jul 1998 13:03:20 +0200 |
berghofe |
Adapted to new datatype package.
|
file |
diff |
annotate
|
| Tue, 09 Jun 1998 13:49:43 +0200 |
wenzelm |
nonterminals prog;
|
file |
diff |
annotate
|
| Fri, 10 Oct 1997 19:02:28 +0200 |
wenzelm |
fixed dots;
|
file |
diff |
annotate
|
| Fri, 04 Apr 1997 14:05:12 +0200 |
nipkow |
renamed variable 'inv'
|
file |
diff |
annotate
|
| Mon, 03 Mar 1997 13:50:40 +0100 |
wenzelm |
added comment: print translations do not mark tokens;
|
file |
diff |
annotate
|
| Wed, 27 Nov 1996 10:41:42 +0100 |
paulson |
Replaced obsolete "makestring" by Int.toString
|
file |
diff |
annotate
|
| Tue, 25 Jun 1996 13:11:29 +0200 |
berghofe |
Changed argument order of nat_rec.
|
file |
diff |
annotate
|
| Fri, 08 Mar 1996 13:11:09 +0100 |
clasohm |
added constdefs section
|
file |
diff |
annotate
|
| Mon, 05 Feb 1996 21:29:06 +0100 |
clasohm |
expanded tabs; incorporated Konrad's changes
|
file |
diff |
annotate
|
| Fri, 01 Dec 1995 14:17:50 +0100 |
clasohm |
removed quotes from types section
|
file |
diff |
annotate
|
| Wed, 29 Nov 1995 17:01:41 +0100 |
clasohm |
removed quotes from consts and syntax sections
|
file |
diff |
annotate
|
| Fri, 17 Nov 1995 09:04:10 +0100 |
nipkow |
New directory.
|
file |
diff |
annotate
|