| 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
|
| Thu, 26 Jun 2008 10:07:01 +0200 |
haftmann |
established Plain theory and image
|
file |
diff |
annotate
|
| Mon, 23 Jun 2008 15:51:38 +0200 |
wenzelm |
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
|
file |
diff |
annotate
|
| Fri, 20 Jun 2008 21:00:16 +0200 |
haftmann |
moved Float.thy to Library
|
file |
diff |
annotate
|
| Thu, 12 Jun 2008 11:51:47 +0200 |
wenzelm |
some reformatting;
|
file |
diff |
annotate
|
| Thu, 12 Jun 2008 10:03:45 +0200 |
urbanc |
added CK_Machine to the nominal section
|
file |
diff |
annotate
|
| Tue, 10 Jun 2008 19:15:20 +0200 |
wenzelm |
added HOL/Tools/induct_tacs.ML;
|
file |
diff |
annotate
|
| Tue, 10 Jun 2008 15:30:06 +0200 |
haftmann |
major refactorings in code generator modules
|
file |
diff |
annotate
|
| Sun, 01 Jun 2008 17:39:21 +0200 |
urbanc |
new example
|
file |
diff |
annotate
|
| Tue, 13 May 2008 09:14:07 +0200 |
krauss |
fixed makefile
|
file |
diff |
annotate
|
| Fri, 25 Apr 2008 15:30:33 +0200 |
krauss |
Merged theories about wellfoundedness into one: Wellfounded.thy
|
file |
diff |
annotate
|
| Tue, 22 Apr 2008 10:31:15 +0200 |
haftmann |
dropped theory PreList
|
file |
diff |
annotate
|
| Tue, 22 Apr 2008 08:33:21 +0200 |
haftmann |
added theory Sublist_Order
|
file |
diff |
annotate
|
| Wed, 16 Apr 2008 17:40:59 +0200 |
wenzelm |
removed unused TLA/Memory/MIParameters.thy;
|
file |
diff |
annotate
|
| Tue, 08 Apr 2008 20:14:36 +0200 |
krauss |
fixed makefiles
|
file |
diff |
annotate
|
| Thu, 20 Mar 2008 12:01:10 +0100 |
haftmann |
added theory Library/Enum.thy
|
file |
diff |
annotate
|
| Fri, 14 Mar 2008 19:57:12 +0100 |
nipkow |
Added lemmas
|
file |
diff |
annotate
|
| Wed, 12 Mar 2008 19:38:14 +0100 |
haftmann |
separated Random.thy from Quickcheck.thy
|
file |
diff |
annotate
|
| Fri, 07 Mar 2008 13:53:01 +0100 |
haftmann |
canonical order on option type
|
file |
diff |
annotate
|
| Tue, 04 Mar 2008 13:35:45 +0100 |
urbanc |
added new example
|
file |
diff |
annotate
|
| Mon, 03 Mar 2008 14:03:19 +0100 |
krauss |
new theory of red-black trees, an efficient implementation of finite maps.
|
file |
diff |
annotate
|
| Wed, 27 Feb 2008 21:41:08 +0100 |
haftmann |
added theories for imperative HOL
|
file |
diff |
annotate
|
| Wed, 27 Feb 2008 14:39:49 +0100 |
chaieb |
HOL/Dense_Linear_Order.thy moved to Library ; resulting dependencies updated
|
file |
diff |
annotate
|
| Mon, 25 Feb 2008 12:05:58 +0100 |
chaieb |
Added dependency of Library on Pocklington.thy
|
file |
diff |
annotate
|
| Mon, 25 Feb 2008 11:26:59 +0100 |
chaieb |
Included theories Library/Univ_Poly.thy and Complex/Fundamental_Theorem_Algebra.thy ; Theory Hyperreal/Poly.thy Removed
|
file |
diff |
annotate
|
| Wed, 20 Feb 2008 23:14:59 +0100 |
wenzelm |
removed ex/NBE.thy;
|
file |
diff |
annotate
|
| Fri, 25 Jan 2008 14:53:56 +0100 |
haftmann |
distinguished examples for Efficient_Nat.thy
|
file |
diff |
annotate
|
| Tue, 15 Jan 2008 16:19:23 +0100 |
haftmann |
joined theories IntDef, Numeral, IntArith to theory Int
|
file |
diff |
annotate
|
| Wed, 02 Jan 2008 15:14:15 +0100 |
haftmann |
improved evaluation mechanism
|
file |
diff |
annotate
|
| Thu, 20 Dec 2007 14:33:40 +0100 |
wenzelm |
moved Pure/General/random_word.ML to Tools/random_word.ML;
|
file |
diff |
annotate
|
| Thu, 20 Dec 2007 12:02:46 +0100 |
wenzelm |
updated HOL-Nominal-Examples deps;
|
file |
diff |
annotate
|
| Tue, 11 Dec 2007 10:23:05 +0100 |
haftmann |
joined EvenOdd theory with Parity
|
file |
diff |
annotate
|
| Fri, 07 Dec 2007 10:59:03 +0100 |
krauss |
Adding "ex/Induction_Scheme.thy" to tests
|
file |
diff |
annotate
|
| Thu, 06 Dec 2007 15:10:09 +0100 |
haftmann |
added new primrec package
|
file |
diff |
annotate
|
| Wed, 05 Dec 2007 14:16:15 +0100 |
haftmann |
dropped Classpackage.thy
|
file |
diff |
annotate
|
| Tue, 13 Nov 2007 10:59:26 +0100 |
berghofe |
Added new program extraction examples.
|
file |
diff |
annotate
|
| Tue, 06 Nov 2007 22:50:39 +0100 |
wenzelm |
activated HOL-SizeChange;
|
file |
diff |
annotate
|
| Tue, 06 Nov 2007 20:27:33 +0100 |
wenzelm |
removed dependencies on Size_Change_Termination from HOL-Library;
|
file |
diff |
annotate
|
| Tue, 06 Nov 2007 17:44:53 +0100 |
krauss |
moved stuff about size change termination to its own session
|
file |
diff |
annotate
|
| Mon, 05 Nov 2007 22:50:48 +0100 |
kleing |
add root.bib for Word document
|
file |
diff |
annotate
|
| Wed, 24 Oct 2007 19:21:39 +0200 |
wenzelm |
fixed HOL-Statespace for case-sensitive file-system;
|
file |
diff |
annotate
|
| Wed, 24 Oct 2007 18:36:09 +0200 |
schirmer |
added Statespace library
|
file |
diff |
annotate
|
| Fri, 12 Oct 2007 08:21:09 +0200 |
haftmann |
consolidated naming conventions for code generator theories
|
file |
diff |
annotate
|
| Mon, 08 Oct 2007 22:03:25 +0200 |
haftmann |
integrated FixedPoint into Inductive
|
file |
diff |
annotate
|
| Mon, 08 Oct 2007 07:09:29 +0200 |
urbanc |
changed VC-Compatible to VC_Compatible
|
file |
diff |
annotate
|
| Mon, 08 Oct 2007 05:27:52 +0200 |
urbanc |
added the two new examples from Nominal to the build process
|
file |
diff |
annotate
|
| Thu, 04 Oct 2007 14:42:47 +0200 |
wenzelm |
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
|
file |
diff |
annotate
|
| Sat, 29 Sep 2007 10:40:12 +0200 |
kleing |
Added target for proof term sessions (those that need -p 2)
|
file |
diff |
annotate
|
| Tue, 25 Sep 2007 12:16:08 +0200 |
haftmann |
datatype interpretators for size and datatype_realizer
|
file |
diff |
annotate
|
| Tue, 18 Sep 2007 18:05:34 +0200 |
wenzelm |
moved Tools/integer.ML to Pure/General/integer.ML;
|
file |
diff |
annotate
|
| Tue, 18 Sep 2007 07:46:00 +0200 |
haftmann |
introduced generic concepts for theory interpretators
|
file |
diff |
annotate
|
| Tue, 18 Sep 2007 07:36:38 +0200 |
haftmann |
separated code for inductive sequences from inductive_codegen.ML
|
file |
diff |
annotate
|
| Tue, 18 Sep 2007 06:21:40 +0200 |
nipkow |
sorting
|
file |
diff |
annotate
|
| Sun, 16 Sep 2007 21:04:44 +0200 |
wenzelm |
added Induct/Common_Patterns.thy;
|
file |
diff |
annotate
|
| Thu, 06 Sep 2007 11:52:13 +0200 |
berghofe |
- New theories Lambda/NormalForm and Lambda/Standardization
|
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
|
| Tue, 28 Aug 2007 20:13:47 +0200 |
huffman |
revert to Word library version from 2007/08/20
|
file |
diff |
annotate
|
| Tue, 28 Aug 2007 18:24:34 +0200 |
berghofe |
codegen.ML is now loaded in Pure again.
|
file |
diff |
annotate
|
| Tue, 28 Aug 2007 03:56:24 +0200 |
huffman |
HOL-Word-Examples
|
file |
diff |
annotate
|
| Thu, 23 Aug 2007 16:47:16 +0200 |
huffman |
Word/BinInduct.thy
|
file |
diff |
annotate
|
| Wed, 22 Aug 2007 21:09:21 +0200 |
huffman |
removed Word/Size.thy;
|
file |
diff |
annotate
|
| Wed, 22 Aug 2007 16:54:43 +0200 |
huffman |
Word/WordBoolList.thy
|
file |
diff |
annotate
|
| Tue, 21 Aug 2007 00:24:10 +0200 |
wenzelm |
use HOL-ex later;
|
file |
diff |
annotate
|
| Mon, 20 Aug 2007 17:34:04 +0200 |
huffman |
Word/document/root.tex
|
file |
diff |
annotate
|
| Mon, 20 Aug 2007 04:34:31 +0200 |
kleing |
* HOL-Word:
|
file |
diff |
annotate
|
| Mon, 20 Aug 2007 00:22:18 +0200 |
kleing |
boolean algebras as locales and numbers as types by Brian Huffman
|
file |
diff |
annotate
|