| Tue, 12 Aug 2003 13:35:03 +0200 |
paulson |
ZhouGollmann: new example (fair non-repudiation protocol)
|
file |
diff |
annotate
|
| Thu, 24 Jul 2003 18:23:17 +0200 |
paulson |
new theory Library/NatPair
|
file |
diff |
annotate
|
| Thu, 17 Jul 2003 15:23:20 +0200 |
skalberg |
Added package for definition by specification.
|
file |
diff |
annotate
|
| Thu, 03 Jul 2003 18:07:50 +0200 |
paulson |
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
|
file |
diff |
annotate
|
| Thu, 03 Jul 2003 12:56:48 +0200 |
paulson |
converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)
|
file |
diff |
annotate
|
| Thu, 03 Jul 2003 10:37:25 +0200 |
paulson |
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
|
file |
diff |
annotate
|
| Thu, 26 Jun 2003 18:20:00 +0200 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Tue, 24 Jun 2003 10:42:34 +0200 |
berghofe |
Added new theories StrongNorm and WeakNorm to Lambda example.
|
file |
diff |
annotate
|
| Mon, 26 May 2003 11:42:41 +0200 |
kleing |
set HOL_PROOF_OBJECTS in settings, not makefile (makes override in user settings possible)
|
file |
diff |
annotate
|
| Sat, 24 May 2003 19:52:53 +0200 |
kleing |
fixed
|
file |
diff |
annotate
|
| Fri, 23 May 2003 17:19:53 +0200 |
kleing |
make it possible to switch off proof objects for HOL image
|
file |
diff |
annotate
|
| Wed, 14 May 2003 20:36:29 +0200 |
schirmer |
Added Bali to test
|
file |
diff |
annotate
|
| Wed, 14 May 2003 15:22:37 +0200 |
kleing |
use proof objects for HOL by default
|
file |
diff |
annotate
|
| Wed, 14 May 2003 10:22:09 +0200 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Thu, 08 May 2003 17:44:38 +0200 |
paulson |
new theory Complex_Main as basis for analysis developments
|
file |
diff |
annotate
|
| Thu, 08 May 2003 13:37:51 +0200 |
kleing |
-> HOL-Complex-HahnBanach in clean target
|
file |
diff |
annotate
|
| Thu, 08 May 2003 13:10:02 +0200 |
paulson |
removed obsolete references to HOL-Real
|
file |
diff |
annotate
|
| Wed, 07 May 2003 14:53:35 +0200 |
kleing |
fixed HOL-Real-HahnBanach (-> HOL-Complex-HahnBanach)
|
file |
diff |
annotate
|
| Tue, 06 May 2003 17:45:54 +0200 |
paulson |
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
|
file |
diff |
annotate
|
| Tue, 06 May 2003 10:47:17 +0200 |
kleing |
fixed missing -g true for HOL-Auth
|
file |
diff |
annotate
|
| Mon, 05 May 2003 18:36:00 +0200 |
paulson |
new directory Complex
|
file |
diff |
annotate
|
| Fri, 02 May 2003 20:02:50 +0200 |
ballarin |
HOL-Algebra complete for release Isabelle2003 (modulo section headers).
|
file |
diff |
annotate
|
| Thu, 01 May 2003 10:29:44 +0200 |
paulson |
moving Bij.thy from GroupTheory to Algebra
|
file |
diff |
annotate
|
| Wed, 30 Apr 2003 18:31:38 +0200 |
ballarin |
HOL-Algebra: new dependencies.
|
file |
diff |
annotate
|
| Sat, 26 Apr 2003 12:38:42 +0200 |
paulson |
converting more HOL-Auth to new-style theories
|
file |
diff |
annotate
|
| Fri, 25 Apr 2003 11:18:41 +0200 |
paulson |
Auth: certified email protocol
|
file |
diff |
annotate
|
| Fri, 11 Apr 2003 23:11:13 +0200 |
webertj |
Map.ML integrated into Map.thy
|
file |
diff |
annotate
|
| Wed, 09 Apr 2003 12:51:49 +0200 |
paulson |
Removal of Summation theory
|
file |
diff |
annotate
|
| Tue, 25 Mar 2003 09:49:45 +0100 |
berghofe |
Added decision procedure for Presburger arithmetic.
|
file |
diff |
annotate
|
| Sun, 23 Mar 2003 11:57:07 +0100 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Fri, 21 Mar 2003 18:15:56 +0100 |
paulson |
quadratic reciprocity files
|
file |
diff |
annotate
|
| Tue, 18 Mar 2003 18:07:06 +0100 |
paulson |
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
|
file |
diff |
annotate
|
| Tue, 11 Mar 2003 15:19:27 +0100 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Mon, 10 Mar 2003 16:21:06 +0100 |
paulson |
New theory ProgressSets. Definition of closure sets
|
file |
diff |
annotate
|
| Thu, 06 Mar 2003 15:08:38 +0100 |
paulson |
new UNITY examples theory
|
file |
diff |
annotate
|
| Tue, 18 Feb 2003 15:09:14 +0100 |
paulson |
new theory Transformers: Meier-Sanders non-interference theory
|
file |
diff |
annotate
|
| Fri, 31 Jan 2003 20:12:44 +0100 |
paulson |
conversion to new-style theories and tidying
|
file |
diff |
annotate
|
| Thu, 30 Jan 2003 18:08:09 +0100 |
paulson |
conversion of UNITY theories to new-style
|
file |
diff |
annotate
|
| Thu, 30 Jan 2003 10:35:56 +0100 |
paulson |
converting more UNITY theories to new-style
|
file |
diff |
annotate
|
| Wed, 29 Jan 2003 16:34:51 +0100 |
paulson |
converted more UNITY theories to new-style
|
file |
diff |
annotate
|
| Wed, 29 Jan 2003 11:02:08 +0100 |
paulson |
converting UNITY to new-style theories
|
file |
diff |
annotate
|
| Mon, 27 Jan 2003 10:39:31 +0100 |
kleing |
fixed missing UNITY files
|
file |
diff |
annotate
|
| Fri, 24 Jan 2003 14:06:49 +0100 |
paulson |
Partial conversion of UNITY to Isar new-style theories
|
file |
diff |
annotate
|
| Wed, 08 Jan 2003 13:49:52 +0100 |
nipkow |
New files in Hoare/
|
file |
diff |
annotate
|
| Wed, 11 Dec 2002 10:12:48 +0100 |
ballarin |
HOL/GroupTheory/Summation.thy added: summation operator for abelian groups.
|
file |
diff |
annotate
|
| Thu, 28 Nov 2002 10:50:42 +0100 |
ballarin |
HOL-Algebra partially ported to Isar.
|
file |
diff |
annotate
|
| Wed, 13 Nov 2002 15:26:19 +0100 |
berghofe |
Added inductive_realizer.
|
file |
diff |
annotate
|
| Sat, 09 Nov 2002 00:12:25 +0100 |
kleing |
Hoare.ML -> hoare.ML
|
file |
diff |
annotate
|
| Wed, 06 Nov 2002 14:02:18 +0100 |
nipkow |
Hoare.ML -> hoare.ML
|
file |
diff |
annotate
|
| Tue, 05 Nov 2002 15:59:17 +0100 |
kleing |
two new Bali files
|
file |
diff |
annotate
|
| Mon, 28 Oct 2002 14:29:51 +0100 |
nipkow |
conversion ML -> thy
|
file |
diff |
annotate
|
| Wed, 23 Oct 2002 16:09:02 +0200 |
streckem |
Added compiler
|
file |
diff |
annotate
|
| Fri, 27 Sep 2002 10:33:47 +0200 |
paulson |
New theory GroupTheory/Module.thy of modules
|
file |
diff |
annotate
|
| Thu, 26 Sep 2002 15:21:38 +0200 |
paulson |
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
|
file |
diff |
annotate
|
| Thu, 26 Sep 2002 10:51:29 +0200 |
paulson |
Converted Fun to Isar style.
|
file |
diff |
annotate
|
| Wed, 25 Sep 2002 07:57:36 +0200 |
nipkow |
Int.thy -> int.thy
|
file |
diff |
annotate
|
| Sat, 31 Aug 2002 14:03:49 +0200 |
paulson |
converted Hyperreal/Zorn to Isar format and moved to Library
|
file |
diff |
annotate
|
| Fri, 23 Aug 2002 07:41:05 +0200 |
nipkow |
Added div+mod cancelling simproc
|
file |
diff |
annotate
|
| Wed, 21 Aug 2002 15:53:30 +0200 |
paulson |
Frederic Blanqui's new "guard" examples
|
file |
diff |
annotate
|
| Thu, 08 Aug 2002 23:46:51 +0200 |
wenzelm |
tuned deps;
|
file |
diff |
annotate
|
| Wed, 07 Aug 2002 16:48:20 +0200 |
berghofe |
Added file Tools/datatype_realizer.ML
|
file |
diff |
annotate
|
| Mon, 05 Aug 2002 14:35:33 +0200 |
berghofe |
Removed theory NatDef.
|
file |
diff |
annotate
|
| Sun, 21 Jul 2002 15:42:30 +0200 |
berghofe |
Added theory for setting up program extraction.
|
file |
diff |
annotate
|
| Wed, 19 Jun 2002 12:39:41 +0200 |
kleing |
LBV instantiantion refactored, streamlined
|
file |
diff |
annotate
|
| Mon, 03 Jun 2002 09:36:30 +0200 |
nipkow |
Added ex/MergeSort
|
file |
diff |
annotate
|
| Tue, 28 May 2002 11:06:06 +0200 |
paulson |
conversion of IntDiv.thy to Isar format
|
file |
diff |
annotate
|
| Fri, 17 May 2002 15:40:59 +0200 |
nipkow |
Turned into Isar theories.
|
file |
diff |
annotate
|
| Wed, 15 May 2002 13:49:51 +0200 |
nipkow |
Divides.ML -> Divides_lemmas.ML
|
file |
diff |
annotate
|
| Fri, 10 May 2002 17:59:55 +0200 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Fri, 10 May 2002 11:55:45 +0200 |
nipkow |
added dep on IMP/Compiler0
|
file |
diff |
annotate
|
| Wed, 08 May 2002 09:14:56 +0200 |
paulson |
some ex files converted to Isar
|
file |
diff |
annotate
|
| Thu, 04 Apr 2002 17:32:52 +0200 |
paulson |
conversion of Induct/{Slist,Sexp} to Isar scripts
|
file |
diff |
annotate
|
| Tue, 02 Apr 2002 14:28:28 +0200 |
paulson |
conversion of some HOL/Induct proof scripts to Isar
|
file |
diff |
annotate
|
| Thu, 14 Mar 2002 16:48:54 +0100 |
paulson |
removed ex/set.ML
|
file |
diff |
annotate
|
| Wed, 06 Mar 2002 17:56:02 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 06 Mar 2002 17:47:51 +0100 |
wenzelm |
added HOL-Hyperreal-ex;
|
file |
diff |
annotate
|
| Tue, 05 Mar 2002 17:09:15 +0100 |
prensani |
Target HoareParallel in IsaMakefile
|
file |
diff |
annotate
|
| Sat, 02 Mar 2002 00:28:55 +0100 |
wenzelm |
temporarily disabled HoareParallel target;
|
file |
diff |
annotate
|
| Fri, 01 Mar 2002 16:24:43 +0100 |
prensani |
Completed annonce of HoareParallel
|
file |
diff |
annotate
|
| Tue, 26 Feb 2002 15:45:32 +0100 |
kleing |
introduces SystemClasses and BVExample
|
file |
diff |
annotate
|
| Tue, 26 Feb 2002 00:24:37 +0100 |
wenzelm |
Isar_examples/W_correct moved to W0;
|
file |
diff |
annotate
|
| Thu, 21 Feb 2002 20:08:09 +0100 |
wenzelm |
theory Option has been assimilated by Datatype;
|
file |
diff |
annotate
|
| Thu, 21 Feb 2002 14:08:09 +0100 |
kleing |
new MicroJava document
|
file |
diff |
annotate
|
| Sat, 16 Feb 2002 20:59:34 +0100 |
wenzelm |
converted/deleted equalities.ML, mono.ML, subset.ML (see Set.thy);
|
file |
diff |
annotate
|
| Tue, 05 Feb 2002 23:18:08 +0100 |
wenzelm |
moved SVC stuff to ex;
|
file |
diff |
annotate
|
| Mon, 28 Jan 2002 17:52:13 +0100 |
schirmer |
Bali added
|
file |
diff |
annotate
|
| Fri, 18 Jan 2002 18:35:39 +0100 |
wenzelm |
fixed document setup of HOL-Library;
|
file |
diff |
annotate
|
| Thu, 17 Jan 2002 19:37:42 +0100 |
nipkow |
Lex dependencies modified
|
file |
diff |
annotate
|
| Sun, 13 Jan 2002 21:09:17 +0100 |
wenzelm |
added HOL/Real/document/root.tex;
|
file |
diff |
annotate
|
| Sun, 13 Jan 2002 19:42:30 +0100 |
wenzelm |
Real/Complex_Numbers.thy;
|
file |
diff |
annotate
|
| Wed, 09 Jan 2002 17:48:40 +0100 |
wenzelm |
converted theory Transitive_Closure;
|
file |
diff |
annotate
|
| Tue, 08 Jan 2002 21:02:15 +0100 |
wenzelm |
HOL-Hyperreal produces an image (again);
|
file |
diff |
annotate
|
| Wed, 19 Dec 2001 00:26:39 +0100 |
wenzelm |
HOL/IMP: include session graph;
|
file |
diff |
annotate
|
| Sun, 16 Dec 2001 00:20:17 +0100 |
kleing |
MicroJava exception merge
|
file |
diff |
annotate
|
| Mon, 10 Dec 2001 15:18:34 +0100 |
berghofe |
Added new files (code generator and examples).
|
file |
diff |
annotate
|
| Sun, 09 Dec 2001 14:36:14 +0100 |
kleing |
HOL/IMP converted to Isar
|
file |
diff |
annotate
|
| Thu, 06 Dec 2001 17:15:53 +0100 |
wenzelm |
include session graph;
|
file |
diff |
annotate
|
| Thu, 06 Dec 2001 00:38:55 +0100 |
wenzelm |
renamed theory Finite to Finite_Set and converted;
|
file |
diff |
annotate
|
| Tue, 04 Dec 2001 17:59:36 +0100 |
wenzelm |
added Higher_Order_Logic.thy;
|
file |
diff |
annotate
|
| Wed, 21 Nov 2001 00:33:04 +0100 |
wenzelm |
theory Inverse_Image converted and moved to Set;
|
file |
diff |
annotate
|
| Tue, 20 Nov 2001 20:54:12 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 16 Nov 2001 18:24:11 +0100 |
paulson |
even more theories from Jacques
|
file |
diff |
annotate
|
| Thu, 15 Nov 2001 16:12:49 +0100 |
paulson |
new theories from Jacques Fleuriot
|
file |
diff |
annotate
|
| Thu, 08 Nov 2001 17:42:43 +0100 |
wenzelm |
ex/document/root.bib;
|
file |
diff |
annotate
|
| Tue, 06 Nov 2001 23:45:34 +0100 |
wenzelm |
renamed Real/ex/Sqrt_Irrational.thy to Real/ex/Sqrt.thy;
|
file |
diff |
annotate
|
| Mon, 05 Nov 2001 13:55:48 +0100 |
paulson |
new Sqrt example
|
file |
diff |
annotate
|
| Sat, 03 Nov 2001 01:35:11 +0100 |
wenzelm |
moved String into Main;
|
file |
diff |
annotate
|
| Fri, 02 Nov 2001 22:01:58 +0100 |
wenzelm |
theory Calculation move to Set;
|
file |
diff |
annotate
|
| Sat, 20 Oct 2001 20:19:47 +0200 |
wenzelm |
document graphs for several sessions;
|
file |
diff |
annotate
|
| Fri, 19 Oct 2001 22:00:08 +0200 |
wenzelm |
got rid of Provers/split_paired_all.ML;
|
file |
diff |
annotate
|
| Sun, 14 Oct 2001 22:08:29 +0200 |
wenzelm |
moved rulify to ObjectLogic;
|
file |
diff |
annotate
|
| Sun, 14 Oct 2001 20:02:11 +0200 |
wenzelm |
removed Ord.thy (now part of HOL.thy).
|
file |
diff |
annotate
|
| Thu, 04 Oct 2001 15:41:43 +0200 |
wenzelm |
$(SRC)/Provers/induct_method.ML replaces Tools/induct_method.ML;
|
file |
diff |
annotate
|
| Wed, 03 Oct 2001 21:03:05 +0200 |
wenzelm |
Tools/induct_attrib.ML now part of Pure;
|
file |
diff |
annotate
|
| Mon, 01 Oct 2001 11:56:40 +0200 |
wenzelm |
added Ordinals example;
|
file |
diff |
annotate
|
| Thu, 27 Sep 2001 22:28:16 +0200 |
wenzelm |
eliminated theories "equalities" and "mono" (made part of "Typedef",
|
file |
diff |
annotate
|
| Thu, 27 Sep 2001 18:45:40 +0200 |
wenzelm |
updated;
|
file |
diff |
annotate
|
| Thu, 27 Sep 2001 15:42:30 +0200 |
wenzelm |
ex/Hilbert_Classical.thy ex/document/root.tex;
|
file |
diff |
annotate
|
| Sat, 01 Sep 2001 00:20:06 +0200 |
wenzelm |
HOL-Real-Hyperreal made a plain session (no longer an image);
|
file |
diff |
annotate
|
| Fri, 31 Aug 2001 16:27:43 +0200 |
berghofe |
Added new files for code generator.
|
file |
diff |
annotate
|