| 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
|
| Wed, 25 Jul 2001 13:13:01 +0200 |
paulson |
partial restructuring to reduce dependence on Axiom of Choice
|
file |
diff |
annotate
|
| Mon, 23 Jul 2001 17:46:40 +0200 |
paulson |
new GroupTheory examples; PiSets moved to GroupTheory, while LocaleGroup deleted
|
file |
diff |
annotate
|
| Tue, 03 Jul 2001 22:11:09 +0200 |
wenzelm |
Library/ROOT.ML moved to Library/Library/ROOT.ML to avoid accidential
|
file |
diff |
annotate
|
| Tue, 03 Jul 2001 15:28:24 +0200 |
paulson |
Locale-based group theory proofs
|
file |
diff |
annotate
|
| Sat, 16 Jun 2001 20:06:42 +0200 |
oheimb |
added NanoJava
|
file |
diff |
annotate
|
| Sun, 10 Jun 2001 08:03:35 +0200 |
paulson |
new GroupTheory example, e.g. the Sylow theorem (preliminary version)
|
file |
diff |
annotate
|
| Sat, 09 Jun 2001 08:41:25 +0200 |
paulson |
moved Primes.thy from NumberTheory to Library
|
file |
diff |
annotate
|
| Fri, 08 Jun 2001 08:50:08 +0200 |
nipkow |
Removed BCV
|
file |
diff |
annotate
|
| Thu, 31 May 2001 20:53:49 +0200 |
wenzelm |
added HOL-CTL;
|
file |
diff |
annotate
|
| Thu, 31 May 2001 16:52:54 +0200 |
oheimb |
added Library/Nat_Infinity.thy and Library/Continuity.thy
|
file |
diff |
annotate
|
| Tue, 08 May 2001 15:56:57 +0200 |
paulson |
conversion of Auth/TLS to Isar script
|
file |
diff |
annotate
|
| Tue, 24 Apr 2001 12:19:01 +0200 |
paulson |
(rough) conversion of Auth/Recur to Isar format
|
file |
diff |
annotate
|
| Thu, 12 Apr 2001 12:45:05 +0200 |
paulson |
converted many HOL/Auth theories to Isar scripts
|
file |
diff |
annotate
|
| Wed, 28 Mar 2001 13:39:50 +0200 |
nipkow |
MicroJava/BV dependencies incomplete
|
file |
diff |
annotate
|
| Fri, 23 Mar 2001 10:10:53 +0100 |
nipkow |
added one point simprocs for bounded quantifiers
|
file |
diff |
annotate
|
| Mon, 05 Mar 2001 15:25:11 +0100 |
paulson |
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
|
file |
diff |
annotate
|
| Fri, 02 Mar 2001 13:26:55 +0100 |
paulson |
conversion of Message.thy to Isar format
|
file |
diff |
annotate
|
| Thu, 15 Feb 2001 16:00:35 +0100 |
oheimb |
Ord.thy/.ML converted to Isar
|
file |
diff |
annotate
|
| Tue, 13 Feb 2001 15:46:03 +0100 |
paulson |
partial conversion to Isar script style in HOL/Auth removes some .ML files
|
file |
diff |
annotate
|
| Fri, 09 Feb 2001 16:22:30 +0100 |
kleing |
removed MicroJava/Digest.thy
|
file |
diff |
annotate
|
| Sun, 04 Feb 2001 19:31:13 +0100 |
wenzelm |
HOL-NumberTheory: converted to new-style format and proper document setup;
|
file |
diff |
annotate
|
| Sat, 03 Feb 2001 17:40:16 +0100 |
wenzelm |
Induct: converted some theories to new-style format;
|
file |
diff |
annotate
|
| Thu, 01 Feb 2001 20:53:13 +0100 |
oheimb |
converted to Isar, simplifying recursion on class hierarchy
|
file |
diff |
annotate
|
| Thu, 01 Feb 2001 20:51:13 +0100 |
wenzelm |
converted to new-style theories;
|
file |
diff |
annotate
|
| Sun, 28 Jan 2001 16:46:19 +0100 |
nipkow |
fixed set comprehension print translation
|
file |
diff |
annotate
|
| Fri, 26 Jan 2001 00:19:50 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 26 Jan 2001 00:15:36 +0100 |
wenzelm |
Transitive_Closure turned into new-style theory;
|
file |
diff |
annotate
|
| Tue, 23 Jan 2001 18:05:53 +0100 |
wenzelm |
added HOL-Unix example;
|
file |
diff |
annotate
|
| Sat, 20 Jan 2001 00:32:56 +0100 |
wenzelm |
added Library/Ring_and_Field_Example.thy;
|
file |
diff |
annotate
|
| Fri, 19 Jan 2001 23:53:07 +0100 |
wenzelm |
added HOL/Library/Nested_Environment.thy;
|
file |
diff |
annotate
|
| Tue, 16 Jan 2001 19:21:21 +0100 |
kleing |
removed obsolete MicroJava/JVM/Store.thy
|
file |
diff |
annotate
|
| Tue, 16 Jan 2001 00:25:25 +0100 |
wenzelm |
removed ex/StringEx.ML;
|
file |
diff |
annotate
|
| Fri, 12 Jan 2001 11:06:50 +0100 |
wenzelm |
added Induct/Sigma_Algebra.thy;
|
file |
diff |
annotate
|
| Sun, 07 Jan 2001 21:40:49 +0100 |
wenzelm |
removed MicroJava/BV/Convert.thy;
|
file |
diff |
annotate
|
| Fri, 05 Jan 2001 10:19:32 +0100 |
paulson |
new UNITY examples by Sidi Ehmety
|
file |
diff |
annotate
|
| Wed, 03 Jan 2001 21:23:13 +0100 |
wenzelm |
TFL: renamed .sml to .ML;
|
file |
diff |
annotate
|
| Mon, 01 Jan 2001 11:51:20 +0100 |
paulson |
put in some missing Hyperreal files
|
file |
diff |
annotate
|
| Sat, 30 Dec 2000 22:03:47 +0100 |
paulson |
separation of HOL-Hyperreal from HOL-Real
|
file |
diff |
annotate
|
| Sat, 23 Dec 2000 22:50:19 +0100 |
wenzelm |
Tools/string_syntax.ML;
|
file |
diff |
annotate
|
| Thu, 21 Dec 2000 19:19:18 +0100 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Tue, 19 Dec 2000 15:19:12 +0100 |
paulson |
new file extract_common_term.ML for the cancel-factor simprocs
|
file |
diff |
annotate
|
| Sat, 16 Dec 2000 21:41:51 +0100 |
wenzelm |
tuned HOL/Real/HahnBanach;
|
file |
diff |
annotate
|
| Wed, 06 Dec 2000 20:05:58 +0100 |
wenzelm |
added Library/Rational_Numbers.thy;
|
file |
diff |
annotate
|
| Fri, 01 Dec 2000 19:53:29 +0100 |
nipkow |
Linear arithmetic now copes with mixed nat/int formulae.
|
file |
diff |
annotate
|
| Wed, 29 Nov 2000 10:19:32 +0100 |
paulson |
new simproc file cancel_numeral_factor.ML
|
file |
diff |
annotate
|
| Fri, 17 Nov 2000 18:47:15 +0100 |
wenzelm |
Library/Ring_and_Field.thy;
|
file |
diff |
annotate
|
| Fri, 10 Nov 2000 19:08:30 +0100 |
wenzelm |
proper theory context for mesontest2;
|
file |
diff |
annotate
|
| Mon, 30 Oct 2000 18:24:20 +0100 |
wenzelm |
added ex/PER.thy;
|
file |
diff |
annotate
|
| Thu, 26 Oct 2000 14:59:38 +0200 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Wed, 25 Oct 2000 18:31:21 +0200 |
wenzelm |
"List prefixes" library theory (replaces old Lex/Prefix);
|
file |
diff |
annotate
|
| Thu, 19 Oct 2000 21:21:20 +0200 |
wenzelm |
added Tools/induct_attrib.ML;
|
file |
diff |
annotate
|
| Wed, 18 Oct 2000 23:44:52 +0200 |
wenzelm |
removed Library/Accessible_Part.ML;
|
file |
diff |
annotate
|
| Wed, 18 Oct 2000 23:33:04 +0200 |
wenzelm |
added HOL/Library, rearranged several files;
|
file |
diff |
annotate
|
| Fri, 13 Oct 2000 08:28:21 +0200 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Thu, 12 Oct 2000 18:38:23 +0200 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Fri, 06 Oct 2000 01:04:56 +0200 |
wenzelm |
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
|
file |
diff |
annotate
|
| Tue, 03 Oct 2000 22:34:49 +0200 |
wenzelm |
added Isar_examples/Hoare.thy Isar_examples/HoareEx.thy;
|
file |
diff |
annotate
|
| Tue, 03 Oct 2000 18:34:20 +0200 |
wenzelm |
reorganized AxClasses;
|
file |
diff |
annotate
|
| Wed, 27 Sep 2000 19:36:31 +0200 |
wenzelm |
proper Hyperreal setup;
|
file |
diff |
annotate
|
| Fri, 22 Sep 2000 13:16:24 +0200 |
kleing |
removed JVM/Store.ML, added theorem Digest in MicroJava
|
file |
diff |
annotate
|
| Thu, 21 Sep 2000 15:58:13 +0200 |
wenzelm |
renamed HOL/ex/Points to HOL/ex/Records;
|
file |
diff |
annotate
|
| Wed, 13 Sep 2000 18:45:10 +0200 |
paulson |
moved Primes, Fib, Factorization to HOL/NumberTheory
|
file |
diff |
annotate
|
| Tue, 12 Sep 2000 10:50:29 +0200 |
wenzelm |
added MicroJava/document/root.bib;
|
file |
diff |
annotate
|
| Thu, 07 Sep 2000 20:48:51 +0200 |
wenzelm |
added Provers/rulify.ML;
|
file |
diff |
annotate
|
| Tue, 05 Sep 2000 21:06:01 +0200 |
wenzelm |
improved meson setup;
|
file |
diff |
annotate
|
| Tue, 05 Sep 2000 10:15:23 +0200 |
paulson |
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
|
file |
diff |
annotate
|
| Mon, 04 Sep 2000 10:24:55 +0200 |
paulson |
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
|
file |
diff |
annotate
|
| Mon, 04 Sep 2000 09:40:28 +0200 |
nipkow |
BCV
|
file |
diff |
annotate
|
| Sat, 02 Sep 2000 22:42:04 +0200 |
wenzelm |
Lambda/document/root.tex;
|
file |
diff |
annotate
|
| Sat, 02 Sep 2000 21:56:24 +0200 |
wenzelm |
HOL/Lambda: converted into new-style theory and document;
|
file |
diff |
annotate
|
| Fri, 01 Sep 2000 00:30:25 +0200 |
wenzelm |
converted Lambda scripts;
|
file |
diff |
annotate
|
| Thu, 31 Aug 2000 01:42:23 +0200 |
wenzelm |
ported HOL/Lambda/ListBeta;
|
file |
diff |
annotate
|
| Wed, 30 Aug 2000 21:44:12 +0200 |
kleing |
MicroJava changed (all of BV -> Isar)
|
file |
diff |
annotate
|
| Tue, 29 Aug 2000 00:57:24 +0200 |
wenzelm |
Lambda/InductTermi made new-style theory;
|
file |
diff |
annotate
|
| Fri, 18 Aug 2000 17:53:49 +0200 |
wenzelm |
Main now new-style theory; added Main.ML for compatibility;
|
file |
diff |
annotate
|
| Thu, 17 Aug 2000 16:23:50 +0200 |
wenzelm |
removed Lambda/Type.ML;
|
file |
diff |
annotate
|
| Mon, 14 Aug 2000 18:08:26 +0200 |
kleing |
added MicroJava/BV/StepMono.thy,
|
file |
diff |
annotate
|
| Mon, 07 Aug 2000 14:34:26 +0200 |
kleing |
MicroJava structure changed
|
file |
diff |
annotate
|
| Thu, 03 Aug 2000 19:28:37 +0200 |
wenzelm |
tuned TLA;
|
file |
diff |
annotate
|
| Thu, 03 Aug 2000 10:53:06 +0200 |
paulson |
new files Integ/IntPower.{thy.ML}; tidied
|
file |
diff |
annotate
|
| Mon, 31 Jul 2000 14:37:18 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 31 Jul 2000 12:50:33 +0200 |
nipkow |
Removed Quot
|
file |
diff |
annotate
|
| Thu, 27 Jul 2000 18:27:25 +0200 |
wenzelm |
added theory While;
|
file |
diff |
annotate
|
| Tue, 25 Jul 2000 00:06:46 +0200 |
wenzelm |
rearranged setup of arithmetic procedures, avoiding global reference values;
|
file |
diff |
annotate
|
| Tue, 18 Jul 2000 13:16:48 +0200 |
kleing |
MicroJava structure changed
|
file |
diff |
annotate
|
| Sun, 16 Jul 2000 20:49:13 +0200 |
wenzelm |
added ex/Tuple.thy;
|
file |
diff |
annotate
|
| Fri, 14 Jul 2000 16:32:51 +0200 |
oheimb |
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
|
file |
diff |
annotate
|
| Fri, 07 Jul 2000 16:46:02 +0200 |
oheimb |
added IMP/Examples.ML dependence
|
file |
diff |
annotate
|
| Wed, 05 Jul 2000 17:52:24 +0200 |
oheimb |
disambiguated := ; added Examples (factorial)
|
file |
diff |
annotate
|
| Tue, 04 Jul 2000 10:54:46 +0200 |
oheimb |
disambiguated := ; added Examples (factorial)
|
file |
diff |
annotate
|
| Wed, 28 Jun 2000 10:37:08 +0200 |
paulson |
new file Provers/make_elim.ML
|
file |
diff |
annotate
|
| Fri, 23 Jun 2000 14:00:43 +0200 |
berghofe |
Added new theory Lambda/Type.
|
file |
diff |
annotate
|
| Wed, 21 Jun 2000 18:09:09 +0200 |
wenzelm |
fixed deps;
|
file |
diff |
annotate
|
| Wed, 07 Jun 2000 12:07:07 +0200 |
paulson |
Real/simproc.ML now removed
|
file |
diff |
annotate
|
| Fri, 02 Jun 2000 12:44:04 +0200 |
oheimb |
added HOL/Prolog
|
file |
diff |
annotate
|
| Wed, 24 May 2000 18:46:38 +0200 |
paulson |
Adding SetInterval, deleting UNITY/LessThan
|
file |
diff |
annotate
|
| Wed, 24 May 2000 12:21:26 +0200 |
paulson |
restored NatSum.thy
|
file |
diff |
annotate
|
| Tue, 23 May 2000 18:24:48 +0200 |
paulson |
IntRingDefs is now redundant
|
file |
diff |
annotate
|
| Tue, 23 May 2000 12:44:03 +0200 |
paulson |
theory file NatSum.thy no longer needed
|
file |
diff |
annotate
|
| Mon, 22 May 2000 16:05:22 +0200 |
wenzelm |
new Isar version of HOL-AxClasses-Tutorial;
|
file |
diff |
annotate
|
| Mon, 22 May 2000 12:28:34 +0200 |
paulson |
new file Induct/MultisetOrder.thy
|
file |
diff |
annotate
|
| Mon, 15 May 2000 10:33:32 +0200 |
paulson |
added the dummy theory Integ/NatSimprocs.thy
|
file |
diff |
annotate
|
| Mon, 08 May 2000 20:59:30 +0200 |
wenzelm |
moved theory Sexp to Induct examples;
|
file |
diff |
annotate
|
| Fri, 05 May 2000 22:25:17 +0200 |
wenzelm |
removed Pure/section_utils.ML;
|
file |
diff |
annotate
|
| Fri, 05 May 2000 12:51:33 +0200 |
nipkow |
Added AVL
|
file |
diff |
annotate
|
| Tue, 02 May 2000 18:40:16 +0200 |
paulson |
combine_numerals replaces both fold_Suc and combine_coeff
|
file |
diff |
annotate
|
| Fri, 21 Apr 2000 11:27:28 +0200 |
paulson |
Provers/Arith/inverse_fold.ML is already obsolete
|
file |
diff |
annotate
|
| Tue, 18 Apr 2000 15:51:59 +0200 |
paulson |
new simprocs for numerals of type "nat"
|
file |
diff |
annotate
|
| Wed, 05 Apr 2000 21:08:24 +0200 |
wenzelm |
added Isar_examples/NestedDatatype.thy;
|
file |
diff |
annotate
|
| Fri, 24 Mar 2000 17:28:03 +0100 |
wenzelm |
added HOL/ex/Multiquote.thy;
|
file |
diff |
annotate
|
| Thu, 23 Mar 2000 11:27:52 +0100 |
wenzelm |
ex/Antiquote.thy made new-style theory;
|
file |
diff |
annotate
|
| Thu, 23 Mar 2000 10:22:08 +0100 |
paulson |
restored the MESON examples file HOL/ex/mesontest2.ML
|
file |
diff |
annotate
|
| Fri, 17 Mar 2000 17:12:07 +0100 |
wenzelm |
fixed dep;
|
file |
diff |
annotate
|
| Thu, 16 Mar 2000 00:35:27 +0100 |
wenzelm |
added HOL/PreLIst.thy;
|
file |
diff |
annotate
|
| Wed, 08 Mar 2000 16:14:12 +0100 |
paulson |
new theory ex/Factorization
|
file |
diff |
annotate
|
| Sat, 04 Mar 2000 11:42:12 +0100 |
paulson |
new theories UNITY/Detects, UNITY/Reachability
|
file |
diff |
annotate
|
| Fri, 18 Feb 2000 15:37:08 +0100 |
paulson |
Rename: theory for applying a bijection over states to a UNITY program
|
file |
diff |
annotate
|
| Fri, 04 Feb 2000 21:45:57 +0100 |
wenzelm |
added MicroJava/document;
|
file |
diff |
annotate
|
| Tue, 01 Feb 2000 18:18:09 +0100 |
oheimb |
added forgotten rules to make IMPP
|
file |
diff |
annotate
|
| Mon, 31 Jan 2000 18:30:35 +0100 |
oheimb |
added IMPP to HOL
|
file |
diff |
annotate
|
| Thu, 20 Jan 2000 17:57:59 +0100 |
wenzelm |
removed Isar_examples/Minimal;
|
file |
diff |
annotate
|
| Mon, 10 Jan 2000 16:06:43 +0100 |
nipkow |
Forgot to "call" MicroJava in makefile.
|
file |
diff |
annotate
|
| Tue, 07 Dec 1999 12:12:54 +0100 |
wenzelm |
added Isar_examples/Fibonacci.thy;
|
file |
diff |
annotate
|
| Tue, 30 Nov 1999 16:51:41 +0100 |
paulson |
new theory UNITY/ELT
|
file |
diff |
annotate
|
| Mon, 29 Nov 1999 11:21:44 +0100 |
wenzelm |
Isar_examples/Minimal.thy;
|
file |
diff |
annotate
|
| Thu, 25 Nov 1999 12:30:57 +0100 |
nipkow |
del Method.ML
|
file |
diff |
annotate
|
| Wed, 17 Nov 1999 15:03:23 +0100 |
wenzelm |
added Isar_examples/Puzzle.thy;
|
file |
diff |
annotate
|
| Thu, 11 Nov 1999 12:24:48 +0100 |
nipkow |
Added MicroJava
|
file |
diff |
annotate
|
| Thu, 11 Nov 1999 11:29:11 +0100 |
wenzelm |
clean target;
|
file |
diff |
annotate
|
| Fri, 05 Nov 1999 12:45:37 +0100 |
paulson |
Algebra and Polynomial theories, by Clemens Ballarin
|
file |
diff |
annotate
|
| Sat, 30 Oct 1999 20:39:01 +0200 |
wenzelm |
fixed deps;
|
file |
diff |
annotate
|
| Thu, 28 Oct 1999 19:53:24 +0200 |
wenzelm |
fixed deps;
|
file |
diff |
annotate
|
| Mon, 25 Oct 1999 19:24:31 +0200 |
wenzelm |
added Real/HahnBanach/document/root.bib;
|
file |
diff |
annotate
|
| Fri, 22 Oct 1999 20:14:31 +0200 |
wenzelm |
HahnBanach update by Gertrud Bauer;
|
file |
diff |
annotate
|
| Fri, 08 Oct 1999 15:08:47 +0200 |
wenzelm |
include document;
|
file |
diff |
annotate
|
| Wed, 06 Oct 1999 18:50:40 +0200 |
wenzelm |
Isar_examples/W_correct;
|
file |
diff |
annotate
|
| Mon, 04 Oct 1999 21:43:05 +0200 |
wenzelm |
removed TFL/sys.sml;
|
file |
diff |
annotate
|
| Tue, 28 Sep 1999 22:17:05 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 28 Sep 1999 16:37:04 +0200 |
nipkow |
added BCV.
|
file |
diff |
annotate
|