| Fri, 15 May 2009 16:52:28 +0200 |
haftmann |
experimental addition of quickcheck
|
file |
diff |
annotate
|
| Fri, 15 May 2009 16:39:17 +0200 |
haftmann |
dropped theory Term_Of_Syntax
|
file |
diff |
annotate
|
| Tue, 12 May 2009 21:17:47 +0200 |
haftmann |
split Predicate_Compile examples into separate theory
|
file |
diff |
annotate
|
| Tue, 12 May 2009 20:07:05 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
| Tue, 12 May 2009 19:30:33 +0200 |
haftmann |
transferred code generator preprocessor into separate module
|
file |
diff |
annotate
|
| Tue, 12 May 2009 17:32:49 +0100 |
chaieb |
Added files Sum_Of_Squares.thy, positivstellensatz.ML and sum_of_squares.ML to Library
|
file |
diff |
annotate
|
| Mon, 11 May 2009 15:18:32 +0200 |
haftmann |
tuned interface of Lin_Arith
|
file |
diff |
annotate
|
| Fri, 08 May 2009 09:48:07 +0200 |
haftmann |
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
|
file |
diff |
annotate
|
| Thu, 07 May 2009 12:17:17 +0200 |
haftmann |
added theory for explicit equivalence relation in preorders
|
file |
diff |
annotate
|
| Wed, 06 May 2009 19:09:31 +0200 |
haftmann |
proper structures for list and string code generation stuff
|
file |
diff |
annotate
|
| Wed, 06 May 2009 16:01:06 +0200 |
haftmann |
refined HOL string theories and corresponding ML fragments
|
file |
diff |
annotate
|
| Mon, 04 May 2009 14:49:51 +0200 |
haftmann |
removed code_name module
|
file |
diff |
annotate
|
| Sat, 25 Apr 2009 21:28:04 +0200 |
wenzelm |
misc cleanup of auto_solve and quickcheck:
|
file |
diff |
annotate
|
| Fri, 24 Apr 2009 17:45:17 +0200 |
haftmann |
observe distinction between Pure/Tools and Tools more closely
|
file |
diff |
annotate
|
| Mon, 20 Apr 2009 09:32:40 +0200 |
haftmann |
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
|
file |
diff |
annotate
|
| Wed, 15 Apr 2009 15:52:37 +0200 |
haftmann |
code generator bootstrap theory src/Tools/Code_Generator.thy
|
file |
diff |
annotate
|
| Wed, 15 Apr 2009 15:34:54 +0200 |
haftmann |
wrecked old code_funcgr module
|
file |
diff |
annotate
|
| Wed, 15 Apr 2009 15:30:39 +0200 |
haftmann |
theory NatBin now named Nat_Numeral
|
file |
diff |
annotate
|
| Mon, 23 Mar 2009 19:01:17 +0100 |
haftmann |
moved Imperative_HOL examples to Imperative_HOL/ex
|
file |
diff |
annotate
|
| Sun, 22 Mar 2009 20:46:11 +0100 |
haftmann |
dropped theory Arith_Tools
|
file |
diff |
annotate
|
| Thu, 12 Mar 2009 23:01:25 +0100 |
haftmann |
merged
|
file |
diff |
annotate
|
| Thu, 12 Mar 2009 18:01:26 +0100 |
haftmann |
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
|
file |
diff |
annotate
|
| Thu, 12 Mar 2009 14:27:21 +0100 |
nipkow |
optional latex sugar
|
file |
diff |
annotate
|
| Wed, 11 Mar 2009 20:11:06 +0100 |
wenzelm |
basic setup for "main" as generated Isabelle manual;
|
file |
diff |
annotate
|
| Wed, 11 Mar 2009 11:41:14 +0100 |
nipkow |
merged
|
file |
diff |
annotate
|
| Wed, 11 Mar 2009 11:40:58 +0100 |
nipkow |
Docs
|
file |
diff |
annotate
|
| Wed, 11 Mar 2009 08:45:47 +0100 |
haftmann |
moved Decision_Procs examples to Decision_Procs/ex
|
file |
diff |
annotate
|
| Mon, 09 Mar 2009 22:56:39 +0100 |
wenzelm |
added session HOL-Docs;
|
file |
diff |
annotate
|
| Sun, 08 Mar 2009 15:25:28 +0100 |
haftmann |
added predicate compiler, as formally checked prototype, not as user package
|
file |
diff |
annotate
|
| Fri, 06 Mar 2009 20:30:16 +0100 |
haftmann |
constructive version of Cantor's first diagonalization argument
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 19:21:55 +0000 |
chaieb |
Added Libray dependency on Topology_Euclidean_Space
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 11:05:29 +0100 |
blanchet |
Merge.
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 10:45:52 +0100 |
blanchet |
Merge.
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 10:47:20 +0100 |
nipkow |
Made Option a separate theory and renamed option_map to Option.map
|
file |
diff |
annotate
|
| Sat, 28 Feb 2009 21:34:33 +0100 |
wenzelm |
A Serbian theory, by Filip Maric.
|
file |
diff |
annotate
|
| Sat, 28 Feb 2009 14:52:21 +0100 |
wenzelm |
moved generic intuitionistic prover to src/Tools/intuitionistic.ML;
|
file |
diff |
annotate
|
| Sat, 28 Feb 2009 14:02:12 +0100 |
wenzelm |
moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete;
|
file |
diff |
annotate
|
| Thu, 26 Feb 2009 14:16:30 +0100 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Wed, 25 Feb 2009 11:26:01 -0800 |
huffman |
new theory of Archimedean fields
|
file |
diff |
annotate
|
| Sun, 22 Feb 2009 10:22:29 +0100 |
haftmann |
formal dependency on newly emerging algorithm
|
file |
diff |
annotate
|
| Fri, 20 Feb 2009 08:02:11 -0800 |
huffman |
add theory of products as real vector spaces to Library
|
file |
diff |
annotate
|
| Fri, 20 Feb 2009 07:41:41 -0800 |
huffman |
add new theory Product_plus.thy to Library
|
file |
diff |
annotate
|
| Thu, 19 Feb 2009 12:03:31 -0800 |
huffman |
add formalization of a type of integers mod 2 to Library
|
file |
diff |
annotate
|
| Thu, 19 Feb 2009 09:42:23 -0800 |
huffman |
new theory of real inner product spaces
|
file |
diff |
annotate
|
| Wed, 18 Feb 2009 20:14:45 -0800 |
huffman |
move Polynomial.thy to Library
|
file |
diff |
annotate
|
| Wed, 18 Feb 2009 19:51:39 -0800 |
huffman |
move FrechetDeriv.thy to Library
|
file |
diff |
annotate
|
| Wed, 18 Feb 2009 19:32:26 -0800 |
huffman |
split polynomial-related stuff from Deriv.thy into Library/Poly_Deriv.thy
|
file |
diff |
annotate
|
| Fri, 13 Feb 2009 09:54:47 +0100 |
nipkow |
Moved Nat_Int_Bij into Library
|
file |
diff |
annotate
|
| Thu, 12 Feb 2009 18:14:43 +0100 |
nipkow |
Moved FTA into Lib and cleaned it up a little.
|
file |
diff |
annotate
|
| Wed, 11 Feb 2009 10:51:07 +0100 |
nipkow |
Moved Order_Relation into Library and moved some of it into Relation.
|
file |
diff |
annotate
|
| Mon, 09 Feb 2009 17:21:46 +0000 |
chaieb |
added Determinants to Library
|
file |
diff |
annotate
|
| Mon, 09 Feb 2009 17:09:18 +0000 |
chaieb |
added Euclidean_Space and Glbs to Library
|
file |
diff |
annotate
|
| Mon, 09 Feb 2009 11:15:13 +0000 |
chaieb |
Added HOL/Library/Finite_Cartesian_Product.thy to Library
|
file |
diff |
annotate
|
| Fri, 06 Feb 2009 15:15:32 +0100 |
haftmann |
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
|
file |
diff |
annotate
|
| Fri, 06 Feb 2009 00:13:15 +0000 |
chaieb |
fixed dependencies : Theory Dense_Linear_Order moved to Library
|
file |
diff |
annotate
|
| Thu, 05 Feb 2009 14:50:43 +0100 |
haftmann |
merged
|
file |
diff |
annotate
|
| Thu, 05 Feb 2009 14:14:02 +0100 |
haftmann |
moved Random.thy to Library
|
file |
diff |
annotate
|
| Thu, 05 Feb 2009 11:49:15 +0100 |
hoelzl |
Add approximation method
|
file |
diff |
annotate
|
| Thu, 05 Feb 2009 11:45:15 +0100 |
hoelzl |
Added new Float theory and moved old Library/Float.thy to ComputeFloat
|
file |
diff |
annotate
|
| Tue, 03 Feb 2009 18:34:49 +0100 |
haftmann |
merged Big0
|
file |
diff |
annotate
|
| Tue, 03 Feb 2009 16:50:41 +0100 |
haftmann |
established session HOL-Reflection
|
file |
diff |
annotate
|
| Mon, 16 Feb 2009 12:27:30 +0100 |
wenzelm |
removed obsolete axclass manual and examples;
|
file |
diff |
annotate
|
| Mon, 02 Feb 2009 13:56:22 +0100 |
haftmann |
added Mapping.thy to Library
|
file |
diff |
annotate
|
| Fri, 30 Jan 2009 17:47:34 +0100 |
krauss |
fixed case
|
file |
diff |
annotate
|
| Fri, 30 Jan 2009 13:24:23 +0000 |
chaieb |
Added Formal_Power_Series_Examples to HOL-ex image
|
file |
diff |
annotate
|
| Thu, 29 Jan 2009 14:56:28 +0000 |
chaieb |
Inserted Formal_Power_Series.thy under Library
|
file |
diff |
annotate
|
| Wed, 28 Jan 2009 11:04:10 +0100 |
haftmann |
Reflection.thy now in HOL/Library
|
file |
diff |
annotate
|
| Mon, 26 Jan 2009 22:14:16 +0100 |
haftmann |
entry point for Word library now named Word
|
file |
diff |
annotate
|
| Sat, 17 Jan 2009 08:28:51 +0100 |
haftmann |
no document for HOL-Base
|
file |
diff |
annotate
|
| Fri, 16 Jan 2009 08:29:11 +0100 |
haftmann |
added HOL-Base image
|
file |
diff |
annotate
|
| Mon, 12 Jan 2009 22:18:51 -0800 |
huffman |
add Polynomial.thy to makefile
|
file |
diff |
annotate
|
| Thu, 08 Jan 2009 17:10:41 +0100 |
haftmann |
split of Imperative_HOL theories from HOL-Library
|
file |
diff |
annotate
|
| Mon, 29 Dec 2008 14:08:08 +0100 |
haftmann |
adapted HOL source structure to distribution layout
|
file |
diff |
annotate
|
| Sat, 27 Dec 2008 17:35:00 +0100 |
krauss |
renamed LexOrds.thy to Termination.thy; examples for sizechange method
|
file |
diff |
annotate
|
| Tue, 16 Dec 2008 08:46:07 +0100 |
krauss |
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
|
file |
diff |
annotate
|
| Mon, 15 Dec 2008 10:19:02 +0100 |
nipkow |
merged
|
file |
diff |
annotate
|
| Thu, 11 Dec 2008 08:52:50 +0100 |
nipkow |
Testfile for Stefan's code generator
|
file |
diff |
annotate
|
| Mon, 15 Dec 2008 09:58:45 +0100 |
haftmann |
moved value.ML to src/Tools
|
file |
diff |
annotate
|
| Wed, 10 Dec 2008 10:23:47 +0100 |
nipkow |
moved ContNotDenum into Library
|
file |
diff |
annotate
|
| Wed, 03 Dec 2008 15:58:44 +0100 |
haftmann |
made repository layout more coherent with logical distribution structure; stripped some $Id$s
|
file |
diff |
annotate
|
| Sat, 29 Nov 2008 13:39:23 +0100 |
nipkow |
new file float_syntax.ML
|
file |
diff |
annotate
|
| Mon, 17 Nov 2008 21:13:48 +0100 |
wenzelm |
removed Induct/Mutil.thy -- the file has been moved to AFP;
|
file |
diff |
annotate
|
| Sat, 15 Nov 2008 21:31:15 +0100 |
wenzelm |
clean: added HOL-Main;
|
file |
diff |
annotate
|
| Thu, 13 Nov 2008 15:59:33 +0100 |
haftmann |
moved assert to Heap_Monad.thy
|
file |
diff |
annotate
|
| Tue, 21 Oct 2008 21:18:54 +0200 |
berghofe |
Added nominal_inductive2.ML
|
file |
diff |
annotate
|
| Fri, 17 Oct 2008 10:39:39 +0200 |
wenzelm |
reactivated HOL-Matrix;
|
file |
diff |
annotate
|
| Thu, 16 Oct 2008 17:52:54 +0200 |
ballarin |
Removed ex/Locales.thy.
|
file |
diff |
annotate
|
| Tue, 14 Oct 2008 16:01:36 +0200 |
wenzelm |
renamed AtpThread to AtpWrapper;
|
file |
diff |
annotate
|
| Sat, 04 Oct 2008 16:05:09 +0200 |
wenzelm |
replaced ISATOOL by ISABELLE_TOOL;
|
file |
diff |
annotate
|
| Fri, 03 Oct 2008 16:37:09 +0200 |
wenzelm |
version of sledgehammer using threads instead of processes, misc cleanup;
|
file |
diff |
annotate
|
| Fri, 03 Oct 2008 15:20:33 +0200 |
wenzelm |
removed old/unused setup of raw ATP oracles;
|
file |
diff |
annotate
|
| Mon, 29 Sep 2008 12:31:58 +0200 |
haftmann |
separate HOL-Main image
|
file |
diff |
annotate
|
| Sun, 28 Sep 2008 14:46:51 +0200 |
wenzelm |
HOL no longer depends on HOL-Plain;
|
file |
diff |
annotate
|
| Sat, 27 Sep 2008 14:26:06 +0200 |
wenzelm |
HOL_USEDIR_OPTIONS no longer applies to HOL-Plain (main HOL is rebuilt from Pure);
|
file |
diff |
annotate
|
| Mon, 22 Sep 2008 23:04:35 +0200 |
berghofe |
Added coherent logic prover.
|
file |
diff |
annotate
|
| Mon, 22 Sep 2008 13:55:59 +0200 |
haftmann |
different session branches for HOL-Plain vs. Plain
|
file |
diff |
annotate
|
| Tue, 16 Sep 2008 16:13:06 +0200 |
haftmann |
moved term_of syntax to separate theory
|
file |
diff |
annotate
|
| Tue, 16 Sep 2008 09:21:22 +0200 |
haftmann |
generic value command
|
file |
diff |
annotate
|
| Wed, 03 Sep 2008 12:11:28 +0200 |
nipkow |
removed ex/Puzzle
|
file |
diff |
annotate
|
| Tue, 02 Sep 2008 22:37:20 +0200 |
nipkow |
Replaced Library/NatPair by Nat_Int_Bij.
|
file |
diff |
annotate
|
| Thu, 28 Aug 2008 22:09:20 +0200 |
haftmann |
restructured and split code serializer module
|
file |
diff |
annotate
|
| Wed, 27 Aug 2008 12:01:59 +0200 |
haftmann |
added HOL/ex/Numeral.thy
|
file |
diff |
annotate
|
| Tue, 05 Aug 2008 14:40:48 +0200 |
krauss |
fix HOL/ex/LexOrds.thy; add to regression
|
file |
diff |
annotate
|
| Fri, 01 Aug 2008 18:10:52 +0200 |
ballarin |
Generalised polynomial lemmas from cring to ring.
|
file |
diff |
annotate
|
| Wed, 30 Jul 2008 19:03:33 +0200 |
ballarin |
New locales for orders and lattices where the equivalence relation is not restricted to equality.
|
file |
diff |
annotate
|
| Tue, 29 Jul 2008 16:16:10 +0200 |
ballarin |
New theory on divisibility;
|
file |
diff |
annotate
|
| Tue, 29 Jul 2008 14:07:23 +0200 |
haftmann |
corrected Pure dependency
|
file |
diff |
annotate
|
| Fri, 25 Jul 2008 12:03:28 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Mon, 21 Jul 2008 15:26:23 +0200 |
haftmann |
(adjusted)
|
file |
diff |
annotate
|
| Wed, 16 Jul 2008 17:37:59 +0200 |
berghofe |
Added Standardization theory to nominal examples.
|
file |
diff |
annotate
|
| Fri, 04 Jul 2008 07:39:01 +0200 |
haftmann |
added marginal setup for code generation
|
file |
diff |
annotate
|
| Thu, 03 Jul 2008 19:50:19 +0200 |
wenzelm |
removed old Complex/ex/NSPrimes.thy;
|
file |
diff |
annotate
|
| Thu, 03 Jul 2008 19:17:29 +0200 |
wenzelm |
more precise dependencies for HOL-Word and HOL-NSA;
|
file |
diff |
annotate
|
| Thu, 03 Jul 2008 17:53:39 +0200 |
huffman |
add HOL-NSA
|
file |
diff |
annotate
|
| Thu, 03 Jul 2008 11:16:33 +0200 |
haftmann |
code antiquotation roaring ahead
|
file |
diff |
annotate
|
| Wed, 02 Jul 2008 07:12:17 +0200 |
haftmann |
code antiquotation roaring ahead
|
file |
diff |
annotate
|
| Tue, 01 Jul 2008 21:20:18 +0200 |
wenzelm |
clean: HOL-Plain;
|
file |
diff |
annotate
|
| Tue, 01 Jul 2008 09:58:32 +0200 |
haftmann |
(removed Complex/ROOT.ML)
|
file |
diff |
annotate
|
| Tue, 01 Jul 2008 07:58:17 +0200 |
haftmann |
HOL += HOL-Complex
|
file |
diff |
annotate
|
| Mon, 30 Jun 2008 13:41:30 +0200 |
haftmann |
HOL-Complex with proof terms
|
file |
diff |
annotate
|