| Thu, 28 Sep 2006 16:01:48 +0200 |
paulson |
clearout of obsolete code
|
file |
diff |
annotate
|
| Tue, 19 Sep 2006 18:18:11 +0200 |
wenzelm |
moved Import/susp.ML to Pure/General;
|
file |
diff |
annotate
|
| Tue, 19 Sep 2006 15:22:21 +0200 |
haftmann |
added OperationalEquality.thy
|
file |
diff |
annotate
|
| Tue, 19 Sep 2006 05:54:17 +0200 |
huffman |
add Real/RealVector.thy
|
file |
diff |
annotate
|
| Thu, 14 Sep 2006 15:25:23 +0200 |
krauss |
updated makefile
|
file |
diff |
annotate
|
| Wed, 30 Aug 2006 08:34:45 +0200 |
haftmann |
added yet another code generator example
|
file |
diff |
annotate
|
| Tue, 29 Aug 2006 14:31:12 +0200 |
haftmann |
added typecopy_package and some examples
|
file |
diff |
annotate
|
| Mon, 21 Aug 2006 11:02:39 +0200 |
haftmann |
added some codegen examples/applications
|
file |
diff |
annotate
|
| Mon, 14 Aug 2006 13:46:08 +0200 |
haftmann |
added new files
|
file |
diff |
annotate
|
| Tue, 08 Aug 2006 08:19:06 +0200 |
haftmann |
added Tools/typedef_codegen.ML
|
file |
diff |
annotate
|
| Thu, 03 Aug 2006 15:03:49 +0200 |
wenzelm |
added HOL/ex/Reflection;
|
file |
diff |
annotate
|
| Thu, 03 Aug 2006 14:57:26 +0200 |
ballarin |
Restructured algebra library, added ideals and quotient rings.
|
file |
diff |
annotate
|
| Tue, 04 Jul 2006 19:49:47 +0200 |
wenzelm |
added ex/Guess.thy;
|
file |
diff |
annotate
|
| Fri, 23 Jun 2006 09:55:01 +0200 |
paulson |
Introduction of Ramsey's theorem
|
file |
diff |
annotate
|
| Sun, 11 Jun 2006 00:42:22 +0200 |
dixon |
updated IsaMakefiles for new location of IsaPlanner.
|
file |
diff |
annotate
|
| Wed, 07 Jun 2006 01:51:22 +0200 |
wenzelm |
removed obsolete ML files;
|
file |
diff |
annotate
|
| Wed, 07 Jun 2006 01:06:53 +0200 |
wenzelm |
removed obsolete ML files;
|
file |
diff |
annotate
|
| Wed, 07 Jun 2006 00:57:14 +0200 |
wenzelm |
removed obsolete ML files;
|
file |
diff |
annotate
|
| Sun, 04 Jun 2006 10:50:41 +0200 |
mengj |
Functions of Tools/ATP/res_clasimpset.ML are now in Tools/res_atp.ML. res_clasimpset.ML is not used anymore.
|
file |
diff |
annotate
|
| Tue, 16 May 2006 13:01:22 +0200 |
wenzelm |
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
|
file |
diff |
annotate
|
| Fri, 05 May 2006 17:17:21 +0200 |
krauss |
First usable version of the new function definition package (HOL/function_packake/...).
|
file |
diff |
annotate
|
| Fri, 28 Apr 2006 17:56:20 +0200 |
berghofe |
Added Class, Fsub, and Lambda_mu examples for nominal datatypes.
|
file |
diff |
annotate
|
| Fri, 28 Apr 2006 15:59:31 +0200 |
berghofe |
Added new targets for nominal datatype package.
|
file |
diff |
annotate
|
| Mon, 10 Apr 2006 16:00:34 +0200 |
obua |
Moved stuff from Ring_and_Field to Matrix
|
file |
diff |
annotate
|
| Mon, 10 Apr 2006 11:35:02 +0200 |
nipkow |
Hoare(Parallel) dependencies on document/*
|
file |
diff |
annotate
|
| Fri, 10 Mar 2006 16:05:34 +0100 |
schirmer |
Added Library/AssocList.thy
|
file |
diff |
annotate
|
| Tue, 07 Mar 2006 16:03:31 +0100 |
obua |
Added HOL-ZF to Isabelle.
|
file |
diff |
annotate
|
| Tue, 07 Mar 2006 03:48:02 +0100 |
mengj |
Merged res_atp_setup.ML into res_atp.ML.
|
file |
diff |
annotate
|
| Wed, 01 Mar 2006 06:06:16 +0100 |
mengj |
Added file Tools/res_atpset.ML.
|
file |
diff |
annotate
|
| Fri, 17 Feb 2006 17:00:33 +0100 |
wenzelm |
removed Import/lazy_scan.ML;
|
file |
diff |
annotate
|
| Thu, 16 Feb 2006 21:11:58 +0100 |
wenzelm |
added ex/Abstract_NAT.thy;
|
file |
diff |
annotate
|
| Tue, 14 Feb 2006 17:07:48 +0100 |
haftmann |
added theory of executable rational numbers
|
file |
diff |
annotate
|
| Wed, 01 Feb 2006 15:22:02 +0100 |
paulson |
new and updated protocol proofs by Giamp Bella
|
file |
diff |
annotate
|
| Fri, 27 Jan 2006 05:45:25 +0100 |
mengj |
Added in new file Tools/ATP/reduce_axiomsN.ML
|
file |
diff |
annotate
|
| Fri, 06 Jan 2006 18:18:15 +0100 |
wenzelm |
removed obsolete eqrule_HOL_data.ML;
|
file |
diff |
annotate
|
| Sat, 31 Dec 2005 21:49:36 +0100 |
wenzelm |
removed obsolete Provers/make_elim.ML;
|
file |
diff |
annotate
|
| Thu, 22 Dec 2005 00:29:15 +0100 |
wenzelm |
added Provers/project_rule.ML
|
file |
diff |
annotate
|
| Wed, 21 Dec 2005 12:06:08 +0100 |
paulson |
new hash table module in HOL/Too/s
|
file |
diff |
annotate
|
| Fri, 16 Dec 2005 12:15:54 +0100 |
paulson |
hashing to eliminate the output of duplicate clauses
|
file |
diff |
annotate
|
| Wed, 14 Dec 2005 22:05:22 +0100 |
webertj |
ex/Sudoku.thy
|
file |
diff |
annotate
|
| Tue, 13 Dec 2005 19:32:04 +0100 |
wenzelm |
added HOL/Library/Coinductive_List.thy;
|
file |
diff |
annotate
|
| Fri, 28 Oct 2005 02:30:53 +0200 |
mengj |
Added Tools/res_hol_clause.ML
|
file |
diff |
annotate
|
| Fri, 21 Oct 2005 02:57:22 +0200 |
mengj |
Merged theory ResAtpOracle.thy into ResAtpMethods.thy
|
file |
diff |
annotate
|
| Wed, 19 Oct 2005 21:52:31 +0200 |
wenzelm |
removed obsolete HOL/thy_syntax.ML;
|
file |
diff |
annotate
|
| Wed, 19 Oct 2005 06:33:24 +0200 |
mengj |
Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover").
|
file |
diff |
annotate
|
| Fri, 14 Oct 2005 11:36:14 +0200 |
paulson |
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
|
file |
diff |
annotate
|
| Mon, 10 Oct 2005 15:35:29 +0200 |
paulson |
small tidy-up of utility functions
|
file |
diff |
annotate
|
| Sat, 08 Oct 2005 22:39:38 +0200 |
wenzelm |
added Import/susp.ML, Import/lazy_seq.ML, Import/lasy_scan.ML;
|
file |
diff |
annotate
|
| Fri, 07 Oct 2005 22:59:21 +0200 |
wenzelm |
removed obsolete ex/Tuple.thy;
|
file |
diff |
annotate
|
| Thu, 29 Sep 2005 00:59:03 +0200 |
wenzelm |
HOL4 image is back;
|
file |
diff |
annotate
|
| Mon, 26 Sep 2005 02:27:59 +0200 |
obua |
added entry for running HOLLight
|
file |
diff |
annotate
|
| Sun, 25 Sep 2005 20:17:13 +0200 |
berghofe |
Added ExecutableSet and Taylor.
|
file |
diff |
annotate
|
| Fri, 23 Sep 2005 22:58:50 +0200 |
webertj |
new sat tactic imports resolution proofs from zChaff
|
file |
diff |
annotate
|
| Fri, 23 Sep 2005 22:21:50 +0200 |
wenzelm |
tuned order of targets;
|
file |
diff |
annotate
|
| Wed, 21 Sep 2005 11:50:20 +0200 |
wenzelm |
HOL-Complex-Matrix: fixed deps;
|
file |
diff |
annotate
|
| Tue, 20 Sep 2005 14:17:31 +0200 |
wenzelm |
HOL-ex: Library/Commutative_Ring.thy;
|
file |
diff |
annotate
|
| Tue, 20 Sep 2005 14:13:20 +0200 |
wenzelm |
moved Tools/comm_ring.ML to Library;
|
file |
diff |
annotate
|
| Tue, 20 Sep 2005 13:58:58 +0200 |
wenzelm |
removed Commutative_Ring.thy, added HOL/ex/Chinese.thy;
|
file |
diff |
annotate
|
| Mon, 19 Sep 2005 19:49:09 +0200 |
obua |
Removed superfluous HOL/Matrix/cplex/ROOT.ML.
|
file |
diff |
annotate
|
| Mon, 19 Sep 2005 18:30:22 +0200 |
paulson |
further simplification of the Isabelle-ATP linkup
|
file |
diff |
annotate
|
| Mon, 19 Sep 2005 15:12:13 +0200 |
paulson |
simplification of the Isabelle-ATP code; hooks for batch generation of problems
|
file |
diff |
annotate
|
| Sat, 17 Sep 2005 18:11:20 +0200 |
wenzelm |
generate: added HOL-Complex-Generate-HOLLight;
|
file |
diff |
annotate
|
| Thu, 15 Sep 2005 23:53:33 +0200 |
huffman |
merge Hyperreal/Transfer.thy and Hyperreal/StarType.thy into Hyperreal/StarDef.thy
|
file |
diff |
annotate
|
| Thu, 15 Sep 2005 17:16:54 +0200 |
wenzelm |
added HOL/ex/Hebrew.thy;
|
file |
diff |
annotate
|
| Wed, 14 Sep 2005 23:14:57 +0200 |
wenzelm |
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
|
file |
diff |
annotate
|
| Wed, 14 Sep 2005 22:04:35 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 14 Sep 2005 17:25:52 +0200 |
chaieb |
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
|
file |
diff |
annotate
|
| Mon, 12 Sep 2005 23:07:58 +0200 |
huffman |
add file Hyperreal/transfer.ML
|
file |
diff |
annotate
|
| Mon, 12 Sep 2005 16:20:18 +0200 |
obua |
1) Added target HOL-Complex-Generate-HOLLight
|
file |
diff |
annotate
|
| Wed, 07 Sep 2005 20:22:15 +0200 |
wenzelm |
removed TLA/Inc/Pcount.thy;
|
file |
diff |
annotate
|
| Wed, 07 Sep 2005 09:53:50 +0200 |
paulson |
consolidation of watcher.ML and watcher.sig
|
file |
diff |
annotate
|
| Tue, 06 Sep 2005 23:14:10 +0200 |
huffman |
add Hyperreal dependencies
|
file |
diff |
annotate
|
| Tue, 06 Sep 2005 18:49:25 +0200 |
wenzelm |
removed some ML files in Modelcheck/;
|
file |
diff |
annotate
|
| Fri, 02 Sep 2005 15:24:58 +0200 |
paulson |
deleted obsolete VampireCommunication.ML
|
file |
diff |
annotate
|
| Wed, 31 Aug 2005 15:46:35 +0200 |
wenzelm |
added Complex/ex/BigO_Complex.thy;
|
file |
diff |
annotate
|
| Fri, 05 Aug 2005 19:56:58 +0200 |
berghofe |
Added Extraction/Pigeonhole.
|
file |
diff |
annotate
|
| Wed, 03 Aug 2005 14:48:30 +0200 |
avigad |
added Hyperreal/Ln, replaced Lfp and Gfp by FixedPoint
|
file |
diff |
annotate
|
| Mon, 25 Jul 2005 18:54:49 +0200 |
avigad |
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
|
file |
diff |
annotate
|
| Tue, 19 Jul 2005 16:16:53 +0200 |
obua |
proving bounds for real linear programs
|
file |
diff |
annotate
|
| Wed, 13 Jul 2005 09:53:50 +0200 |
obua |
- added cplex package to HOL/Matrix
|
file |
diff |
annotate
|
| Tue, 12 Jul 2005 21:49:38 +0200 |
obua |
- use TableFun instead of homebrew binary tree in am_interpreter.ML
|
file |
diff |
annotate
|
| Thu, 07 Jul 2005 12:39:17 +0200 |
nipkow |
linear arithmetic now takes "&" in assumptions apart.
|
file |
diff |
annotate
|
| Tue, 21 Jun 2005 09:31:57 +0200 |
wenzelm |
fixed HOL-Complex-Matrix target;
|
file |
diff |
annotate
|
| Mon, 20 Jun 2005 22:13:57 +0200 |
wenzelm |
HOL-Matrix: plain session;
|
file |
diff |
annotate
|
| Thu, 09 Jun 2005 23:33:28 +0200 |
wenzelm |
added Isar_examples/Drinker.thy;
|
file |
diff |
annotate
|
| Thu, 02 Jun 2005 18:29:47 +0200 |
wenzelm |
renamed HOL_PROOF_OBJECTS to HOL_USEDIR_OPTIONS;
|
file |
diff |
annotate
|
| Thu, 26 May 2005 16:50:20 +0200 |
paulson |
goodby to modUnix
|
file |
diff |
annotate
|
| Sun, 22 May 2005 16:51:07 +0200 |
wenzelm |
Simplifier already setup in Pure;
|
file |
diff |
annotate
|
| Thu, 28 Apr 2005 17:08:08 +0200 |
bauerg |
*** empty log message ***
|
file |
diff |
annotate
|
| Wed, 27 Apr 2005 06:03:35 +0200 |
kleing |
reverted last change (dependencies in HOL)
|
file |
diff |
annotate
|
| Wed, 20 Apr 2005 16:03:17 +0200 |
quigley |
Removed remaining references to Main.thy in reconstruction code.
|
file |
diff |
annotate
|
| Tue, 19 Apr 2005 18:08:44 +0200 |
paulson |
more tidying of libraries in Reconstruction
|
file |
diff |
annotate
|
| Tue, 19 Apr 2005 13:34:50 +0200 |
paulson |
restored the target HOL-Complex-Import
|
file |
diff |
annotate
|
| Thu, 14 Apr 2005 17:57:04 +0200 |
nipkow |
Removed dir Orderings in Library
|
file |
diff |
annotate
|
| Mon, 11 Apr 2005 16:25:31 +0200 |
paulson |
removal of Main and other tidying up
|
file |
diff |
annotate
|
| Fri, 08 Apr 2005 18:43:39 +0200 |
paulson |
Reconstruction code, now packaged to avoid name clashes
|
file |
diff |
annotate
|
| Thu, 07 Apr 2005 17:45:51 +0200 |
quigley |
Reconstruction.thy and IsaMakefile updated
|
file |
diff |
annotate
|
| Mon, 04 Apr 2005 18:43:18 +0200 |
quigley |
Updated to add watcher code.
|
file |
diff |
annotate
|
| Fri, 01 Apr 2005 18:59:17 +0200 |
skalberg |
Updated import configuration.
|
file |
diff |
annotate
|
| Tue, 29 Mar 2005 12:30:48 +0200 |
paulson |
converted HOL-Subst to tactic scripts
|
file |
diff |
annotate
|
| Thu, 24 Mar 2005 16:34:15 +0100 |
ballarin |
Transitivity reasoner ignores types amenable to linear arithmetic.
|
file |
diff |
annotate
|
| Thu, 24 Mar 2005 10:59:21 +0100 |
paulson |
COMMENT IN WRONG PLACE
|
file |
diff |
annotate
|
| Wed, 23 Mar 2005 12:08:52 +0100 |
paulson |
temporary removal of Import
|
file |
diff |
annotate
|
| Mon, 07 Mar 2005 18:19:55 +0100 |
obua |
Cleaning up HOL/Matrix
|
file |
diff |
annotate
|
| Thu, 03 Mar 2005 12:43:01 +0100 |
skalberg |
Move towards standard functions.
|
file |
diff |
annotate
|
| Sun, 13 Feb 2005 17:15:14 +0100 |
skalberg |
Deleted Library.option type.
|
file |
diff |
annotate
|
| Wed, 09 Feb 2005 18:51:02 +0100 |
nipkow |
added lattice_locales
|
file |
diff |
annotate
|
| Tue, 01 Feb 2005 18:01:57 +0100 |
paulson |
the new subst tactic, by Lucas Dixon
|
file |
diff |
annotate
|
| Fri, 17 Dec 2004 10:15:46 +0100 |
paulson |
removed two looping simplifications in SetInterval.thy; deleted the .ML file
|
file |
diff |
annotate
|
| Wed, 15 Dec 2004 10:19:01 +0100 |
paulson |
removal of HOL_Lemmas
|
file |
diff |
annotate
|
| Tue, 14 Dec 2004 14:53:02 +0100 |
paulson |
converted Relation_Power to new-style theory
|
file |
diff |
annotate
|
| Mon, 13 Dec 2004 15:06:59 +0100 |
paulson |
removal of NatArith.ML and Product_Type.ML
|
file |
diff |
annotate
|
| Thu, 09 Dec 2004 16:45:46 +0100 |
paulson |
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
|
file |
diff |
annotate
|
| Thu, 09 Dec 2004 12:03:06 +0100 |
paulson |
converted Datatype_Universe to new-style theory
|
file |
diff |
annotate
|
| Wed, 08 Dec 2004 10:28:05 +0100 |
paulson |
converted Lfp to new-style theory
|
file |
diff |
annotate
|
| Tue, 07 Dec 2004 16:15:44 +0100 |
paulson |
converted Gfp to new-style theory
|
file |
diff |
annotate
|
| Thu, 02 Dec 2004 11:09:19 +0100 |
paulson |
new CLAUSIFY attribute for proof reconstruction with lemmas
|
file |
diff |
annotate
|
| Tue, 30 Nov 2004 18:25:55 +0100 |
paulson |
resolution package tools by Jia Meng
|
file |
diff |
annotate
|
| Tue, 30 Nov 2004 16:27:44 +0100 |
paulson |
converted Wellfounded_Relations to Isar script
|
file |
diff |
annotate
|
| Mon, 29 Nov 2004 14:02:55 +0100 |
paulson |
converted to Isar script, simplifying some results
|
file |
diff |
annotate
|
| Wed, 24 Nov 2004 10:28:09 +0100 |
berghofe |
Added Library/EfficientNat
|
file |
diff |
annotate
|
| Fri, 19 Nov 2004 17:31:49 +0100 |
paulson |
moved and renamed Integ/Equiv.thy
|
file |
diff |
annotate
|
| Fri, 19 Nov 2004 14:00:31 +0100 |
chaieb |
Barith removed
|
file |
diff |
annotate
|
| Wed, 06 Oct 2004 13:58:08 +0200 |
chaieb |
changed in order to insert Barith.thy
|
file |
diff |
annotate
|
| Fri, 10 Sep 2004 20:04:14 +0200 |
nipkow |
Added antisymmetry simproc
|
file |
diff |
annotate
|
| Fri, 03 Sep 2004 17:10:36 +0200 |
obua |
Matrix theory, linear programming
|
file |
diff |
annotate
|
| Thu, 02 Sep 2004 16:52:21 +0200 |
paulson |
new example of a quotiented nested data type
|
file |
diff |
annotate
|
| Fri, 20 Aug 2004 12:20:09 +0200 |
paulson |
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
|
file |
diff |
annotate
|
| Tue, 03 Aug 2004 14:47:51 +0200 |
ballarin |
New transitivity reasoners for transitivity only and quasi orders.
|
file |
diff |
annotate
|
| Sat, 31 Jul 2004 20:54:23 +0200 |
paulson |
conversion of Hyperreal/{Fact,Filter} to Isar scripts
|
file |
diff |
annotate
|
| Fri, 30 Jul 2004 18:37:58 +0200 |
paulson |
conversion of Integration and NSPrimes to Isar scripts
|
file |
diff |
annotate
|
| Wed, 28 Jul 2004 16:26:27 +0200 |
paulson |
conversion of SEQ.ML to Isar script
|
file |
diff |
annotate
|
| Wed, 28 Jul 2004 10:49:29 +0200 |
paulson |
conversion of Hyperreal/MacLaurin_lemmas to Isar script
|
file |
diff |
annotate
|
| Mon, 26 Jul 2004 17:34:52 +0200 |
paulson |
converting Hyperreal/Transcendental to Isar script
|
file |
diff |
annotate
|
| Mon, 26 Jul 2004 15:48:50 +0200 |
ballarin |
New prover for transitive and reflexive-transitive closure of relations.
|
file |
diff |
annotate
|
| Fri, 16 Jul 2004 17:33:43 +0200 |
nipkow |
added Complex/root
|
file |
diff |
annotate
|
| Mon, 12 Jul 2004 12:11:46 +0200 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Thu, 01 Jul 2004 12:29:53 +0200 |
paulson |
new treatment of binary numerals
|
file |
diff |
annotate
|
| Tue, 29 Jun 2004 10:07:56 +0200 |
obua |
support for sparse matrices
|
file |
diff |
annotate
|
| Sat, 29 May 2004 15:10:30 +0200 |
wenzelm |
target 'generate';
|
file |
diff |
annotate
|
| Wed, 19 May 2004 11:29:47 +0200 |
paulson |
conversion of Hilbert_Choice to Isar script
|
file |
diff |
annotate
|
| Tue, 18 May 2004 10:01:44 +0200 |
obua |
Modification / Installation of Provers/Arith/abel_cancel.ML for OrderedGroup.thy
|
file |
diff |
annotate
|
| Tue, 11 May 2004 20:11:08 +0200 |
obua |
changes made due to new Ring_and_Field theory
|
file |
diff |
annotate
|
| Fri, 07 May 2004 14:10:14 +0200 |
bauerg |
*** empty log message ***
|
file |
diff |
annotate
|
| Fri, 23 Apr 2004 20:50:16 +0200 |
wenzelm |
HOL-Matrix: document setup;
|
file |
diff |
annotate
|
| Thu, 22 Apr 2004 10:45:56 +0200 |
paulson |
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
|
file |
diff |
annotate
|
| Mon, 19 Apr 2004 09:31:00 +0200 |
kleing |
renamed HOL-Import-HOL to HOL4, added to images target
|
file |
diff |
annotate
|
| Sat, 17 Apr 2004 00:46:22 +0200 |
kleing |
added HOL-Matrix, added HOL/Matrix/ROOT.ML
|
file |
diff |
annotate
|
| Fri, 16 Apr 2004 20:33:16 +0200 |
nipkow |
Moved ring stuff from ex into Ring_and_Field.
|
file |
diff |
annotate
|
| Fri, 16 Apr 2004 18:09:24 +0200 |
berghofe |
Added theory with examples for quickcheck command.
|
file |
diff |
annotate
|
| Fri, 16 Apr 2004 04:08:29 +0200 |
wenzelm |
session graph;
|
file |
diff |
annotate
|
| Thu, 15 Apr 2004 14:17:45 +0200 |
nipkow |
Added ex/Exceptions.thy
|
file |
diff |
annotate
|
| Tue, 13 Apr 2004 09:42:40 +0200 |
ballarin |
Various changes to HOL-Algebra;
|
file |
diff |
annotate
|
| Thu, 08 Apr 2004 12:49:23 +0200 |
paulson |
new theory
|
file |
diff |
annotate
|
| Fri, 02 Apr 2004 17:37:45 +0200 |
skalberg |
Added HOL proof importer.
|
file |
diff |
annotate
|
| Fri, 02 Apr 2004 17:36:01 +0200 |
webertj |
Tools/sat_solver.ML and Tools/prop_logic.ML added
|
file |
diff |
annotate
|
| Thu, 01 Apr 2004 15:05:04 +0200 |
paulson |
removal of Binary Trees examples prepratory to its going into AFP
|
file |
diff |
annotate
|
| Wed, 31 Mar 2004 11:02:00 +0200 |
nipkow |
Lex now in AFP
|
file |
diff |
annotate
|
| Mon, 29 Mar 2004 15:35:04 +0200 |
skalberg |
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
|
file |
diff |
annotate
|
| Thu, 25 Mar 2004 05:37:32 +0100 |
kleing |
moved MiniML and AVL to archive of formal proofs
|
file |
diff |
annotate
|
| Fri, 19 Mar 2004 10:51:03 +0100 |
paulson |
conversion of Hyperreal/Lim to new-style
|
file |
diff |
annotate
|
| Mon, 08 Mar 2004 11:11:58 +0100 |
paulson |
new theory of infinite sets
|
file |
diff |
annotate
|
| Sat, 06 Mar 2004 19:32:21 +0100 |
nipkow |
Lex: removed last ML files
|
file |
diff |
annotate
|
| Fri, 05 Mar 2004 15:18:59 +0100 |
paulson |
Conversion of Poly to Isar script, and other tidying of HOL/Hyperreal
|
file |
diff |
annotate
|
| Thu, 04 Mar 2004 15:49:42 +0100 |
nipkow |
Lex: ML -> thy
|
file |
diff |
annotate
|
| Thu, 04 Mar 2004 12:06:07 +0100 |
paulson |
new material from Avigad, and simplified treatment of division by 0
|
file |
diff |
annotate
|
| Thu, 04 Mar 2004 10:06:13 +0100 |
nipkow |
Removed ML files from Lex
|
file |
diff |
annotate
|
| Tue, 02 Mar 2004 11:05:55 +0100 |
paulson |
converted Hyperreal/IntFloor to Isar script
|
file |
diff |
annotate
|
| Tue, 02 Mar 2004 01:34:54 +0100 |
kleing |
converted MiniML to Isar
|
file |
diff |
annotate
|
| Mon, 01 Mar 2004 11:52:59 +0100 |
paulson |
converted Hyperreal/HTranscendental to Isar script
|
file |
diff |
annotate
|
| Mon, 01 Mar 2004 05:39:32 +0100 |
kleing |
converted to Isar
|
file |
diff |
annotate
|
| Thu, 26 Feb 2004 17:08:23 +0100 |
paulson |
converted Hyperreal/Series to Isar script
|
file |
diff |
annotate
|
| Thu, 26 Feb 2004 11:31:36 +0100 |
paulson |
converted Hyperreal/NatStar to Isar script
|
file |
diff |
annotate
|
| Wed, 25 Feb 2004 16:22:36 +0100 |
paulson |
converted Hyperreal/HSeries to Isar script
|
file |
diff |
annotate
|
| Tue, 24 Feb 2004 16:38:51 +0100 |
paulson |
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
|
file |
diff |
annotate
|
| Mon, 23 Feb 2004 17:33:38 +0100 |
paulson |
converted HOL/Complex/NSInduct to Isar script
|
file |
diff |
annotate
|
| Mon, 23 Feb 2004 16:35:46 +0100 |
paulson |
converted HOL/Complex/NSCA to Isar script
|
file |
diff |
annotate
|
| Sat, 21 Feb 2004 20:05:16 +0100 |
paulson |
conversion of Complex/CStar to Isar script
|
file |
diff |
annotate
|
| Sat, 21 Feb 2004 15:54:32 +0100 |
paulson |
conversion of Complex/CSeries to Isar script
|
file |
diff |
annotate
|
| Sat, 21 Feb 2004 11:43:39 +0100 |
paulson |
conversion of Complex/CLim to Isar script
|
file |
diff |
annotate
|
| Thu, 19 Feb 2004 15:57:34 +0100 |
ballarin |
Efficient, graph-based reasoner for linear and partial orders.
|
file |
diff |
annotate
|
| Sun, 15 Feb 2004 10:46:37 +0100 |
paulson |
Polymorphic treatment of binary arithmetic using axclasses
|
file |
diff |
annotate
|
| Tue, 10 Feb 2004 12:02:11 +0100 |
paulson |
generic of_nat and of_int functions, and generalization of iszero
|
file |
diff |
annotate
|
| Tue, 03 Feb 2004 11:06:36 +0100 |
paulson |
tidying of the complex numbers
|
file |
diff |
annotate
|
| Mon, 02 Feb 2004 12:23:46 +0100 |
paulson |
Conversion of HyperNat to Isar format and its declaration as a semiring
|
file |
diff |
annotate
|
| Thu, 29 Jan 2004 16:51:17 +0100 |
paulson |
simplifications in the hyperreals
|
file |
diff |
annotate
|
| Wed, 28 Jan 2004 17:01:01 +0100 |
paulson |
tidying up arithmetic for the hyperreals
|
file |
diff |
annotate
|
| Wed, 28 Jan 2004 10:41:49 +0100 |
paulson |
converted Real/Lubs to Isar script. Converting arithmetic setup
|
file |
diff |
annotate
|
| Tue, 27 Jan 2004 15:39:51 +0100 |
paulson |
replacing HOL/Real/PRat, PNat by the rational number development
|
file |
diff |
annotate
|
| Wed, 14 Jan 2004 00:13:04 +0100 |
nipkow |
Told linear arithmetic package about injections "real" from nat/int into real.
|
file |
diff |
annotate
|
| Mon, 12 Jan 2004 16:51:45 +0100 |
paulson |
Added lemmas to Ring_and_Field with slightly modified simplification rules
|
file |
diff |
annotate
|
| Sat, 10 Jan 2004 13:35:10 +0100 |
webertj |
Adding 'refute' to HOL.
|
file |
diff |
annotate
|
| Fri, 09 Jan 2004 10:46:18 +0100 |
paulson |
Defining the type class "ringpower" and deleting superseded theorems for
|
file |
diff |
annotate
|
| Thu, 01 Jan 2004 21:47:07 +0100 |
paulson |
conversion of Real/PReal to Isar script;
|
file |
diff |
annotate
|
| Thu, 01 Jan 2004 10:06:32 +0100 |
paulson |
tweaking of lemmas in RealDef, RealOrd
|
file |
diff |
annotate
|
| Tue, 23 Dec 2003 17:41:52 +0100 |
paulson |
converting Hyperreal/NthRoot to Isar
|
file |
diff |
annotate
|
| Tue, 23 Dec 2003 16:53:33 +0100 |
paulson |
converting Complex/Complex.ML to Isar
|
file |
diff |
annotate
|
| Tue, 23 Dec 2003 14:45:47 +0100 |
paulson |
tidying up hcomplex arithmetic
|
file |
diff |
annotate
|
| Mon, 22 Dec 2003 18:29:20 +0100 |
paulson |
converted Complex/NSComplex to Isar script
|
file |
diff |
annotate
|
| Mon, 22 Dec 2003 12:50:22 +0100 |
paulson |
moving HyperArith0.ML to other theories
|
file |
diff |
annotate
|
| Wed, 17 Dec 2003 16:23:52 +0100 |
paulson |
converted Hyperreal/HyperDef to Isar script
|
file |
diff |
annotate
|
| Tue, 16 Dec 2003 15:38:09 +0100 |
paulson |
converted Hyperreal/HyperOrd to new-style theory
|
file |
diff |
annotate
|
| Wed, 10 Dec 2003 16:47:50 +0100 |
paulson |
combining Real/{RealArith0,real_arith}.ML
|
file |
diff |
annotate
|
| Wed, 10 Dec 2003 15:59:34 +0100 |
paulson |
Moving some theorems from Real/RealArith0.ML
|
file |
diff |
annotate
|
| Thu, 04 Dec 2003 16:16:36 +0100 |
paulson |
further simplifications of the integer development; converting more .ML files
|
file |
diff |
annotate
|
| Thu, 04 Dec 2003 10:29:17 +0100 |
paulson |
Tidying of the integer development; towards removing the
|
file |
diff |
annotate
|
| Fri, 28 Nov 2003 12:09:37 +0100 |
paulson |
conversion of some Real theories to Isar scripts
|
file |
diff |
annotate
|
| Thu, 27 Nov 2003 10:47:55 +0100 |
paulson |
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
|
file |
diff |
annotate
|
| Tue, 25 Nov 2003 10:37:03 +0100 |
paulson |
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
|
file |
diff |
annotate
|
| Mon, 24 Nov 2003 15:33:07 +0100 |
paulson |
conversion of integers to use Ring_and_Field;
|
file |
diff |
annotate
|
| Fri, 21 Nov 2003 11:15:40 +0100 |
paulson |
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
|
file |
diff |
annotate
|
| Thu, 20 Nov 2003 10:42:00 +0100 |
paulson |
conversion of Integ/Int_lemmas.ML to Isar script
|
file |
diff |
annotate
|
| Tue, 18 Nov 2003 11:01:52 +0100 |
paulson |
conversion of ML to Isar scripts
|
file |
diff |
annotate
|
| Wed, 22 Oct 2003 10:52:36 +0200 |
paulson |
InductiveInvariant_examples illustrates advanced recursive function definitions
|
file |
diff |
annotate
|
| Wed, 08 Oct 2003 15:57:41 +0200 |
paulson |
Merging of ex/cla.ML and ex/mesontest.ML to ex/Classical.thy
|
file |
diff |
annotate
|
| Tue, 23 Sep 2003 15:40:27 +0200 |
paulson |
new session HOL-SET-Protocol
|
file |
diff |
annotate
|
| Thu, 04 Sep 2003 11:15:53 +0200 |
paulson |
conversion of HOL/Auth/KerberosIV to new-style theory
|
file |
diff |
annotate
|
| Fri, 15 Aug 2003 13:07:01 +0200 |
paulson |
A document for UNITY
|
file |
diff |
annotate
|
| 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
|