src/HOL/IsaMakefile
Tue, 19 Sep 2006 05:54:17 +0200 huffman add Real/RealVector.thy
Thu, 14 Sep 2006 15:25:23 +0200 krauss updated makefile
Wed, 30 Aug 2006 08:34:45 +0200 haftmann added yet another code generator example
Tue, 29 Aug 2006 14:31:12 +0200 haftmann added typecopy_package and some examples
Mon, 21 Aug 2006 11:02:39 +0200 haftmann added some codegen examples/applications
Mon, 14 Aug 2006 13:46:08 +0200 haftmann added new files
Tue, 08 Aug 2006 08:19:06 +0200 haftmann added Tools/typedef_codegen.ML
Thu, 03 Aug 2006 15:03:49 +0200 wenzelm added HOL/ex/Reflection;
Thu, 03 Aug 2006 14:57:26 +0200 ballarin Restructured algebra library, added ideals and quotient rings.
Tue, 04 Jul 2006 19:49:47 +0200 wenzelm added ex/Guess.thy;
Fri, 23 Jun 2006 09:55:01 +0200 paulson Introduction of Ramsey's theorem
Sun, 11 Jun 2006 00:42:22 +0200 dixon updated IsaMakefiles for new location of IsaPlanner.
Wed, 07 Jun 2006 01:51:22 +0200 wenzelm removed obsolete ML files;
Wed, 07 Jun 2006 01:06:53 +0200 wenzelm removed obsolete ML files;
Wed, 07 Jun 2006 00:57:14 +0200 wenzelm removed obsolete ML files;
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.
Tue, 16 May 2006 13:01:22 +0200 wenzelm added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
Fri, 05 May 2006 17:17:21 +0200 krauss First usable version of the new function definition package (HOL/function_packake/...).
Fri, 28 Apr 2006 17:56:20 +0200 berghofe Added Class, Fsub, and Lambda_mu examples for nominal datatypes.
Fri, 28 Apr 2006 15:59:31 +0200 berghofe Added new targets for nominal datatype package.
Mon, 10 Apr 2006 16:00:34 +0200 obua Moved stuff from Ring_and_Field to Matrix
Mon, 10 Apr 2006 11:35:02 +0200 nipkow Hoare(Parallel) dependencies on document/*
Fri, 10 Mar 2006 16:05:34 +0100 schirmer Added Library/AssocList.thy
Tue, 07 Mar 2006 16:03:31 +0100 obua Added HOL-ZF to Isabelle.
Tue, 07 Mar 2006 03:48:02 +0100 mengj Merged res_atp_setup.ML into res_atp.ML.
Wed, 01 Mar 2006 06:06:16 +0100 mengj Added file Tools/res_atpset.ML.
Fri, 17 Feb 2006 17:00:33 +0100 wenzelm removed Import/lazy_scan.ML;
Thu, 16 Feb 2006 21:11:58 +0100 wenzelm added ex/Abstract_NAT.thy;
Tue, 14 Feb 2006 17:07:48 +0100 haftmann added theory of executable rational numbers
Wed, 01 Feb 2006 15:22:02 +0100 paulson new and updated protocol proofs by Giamp Bella
Fri, 27 Jan 2006 05:45:25 +0100 mengj Added in new file Tools/ATP/reduce_axiomsN.ML
Fri, 06 Jan 2006 18:18:15 +0100 wenzelm removed obsolete eqrule_HOL_data.ML;
Sat, 31 Dec 2005 21:49:36 +0100 wenzelm removed obsolete Provers/make_elim.ML;
Thu, 22 Dec 2005 00:29:15 +0100 wenzelm added Provers/project_rule.ML
Wed, 21 Dec 2005 12:06:08 +0100 paulson new hash table module in HOL/Too/s
Fri, 16 Dec 2005 12:15:54 +0100 paulson hashing to eliminate the output of duplicate clauses
Wed, 14 Dec 2005 22:05:22 +0100 webertj ex/Sudoku.thy
Tue, 13 Dec 2005 19:32:04 +0100 wenzelm added HOL/Library/Coinductive_List.thy;
Fri, 28 Oct 2005 02:30:53 +0200 mengj Added Tools/res_hol_clause.ML
Fri, 21 Oct 2005 02:57:22 +0200 mengj Merged theory ResAtpOracle.thy into ResAtpMethods.thy
Wed, 19 Oct 2005 21:52:31 +0200 wenzelm removed obsolete HOL/thy_syntax.ML;
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").
Fri, 14 Oct 2005 11:36:14 +0200 paulson deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
Mon, 10 Oct 2005 15:35:29 +0200 paulson small tidy-up of utility functions
Sat, 08 Oct 2005 22:39:38 +0200 wenzelm added Import/susp.ML, Import/lazy_seq.ML, Import/lasy_scan.ML;
Fri, 07 Oct 2005 22:59:21 +0200 wenzelm removed obsolete ex/Tuple.thy;
Thu, 29 Sep 2005 00:59:03 +0200 wenzelm HOL4 image is back;
Mon, 26 Sep 2005 02:27:59 +0200 obua added entry for running HOLLight
Sun, 25 Sep 2005 20:17:13 +0200 berghofe Added ExecutableSet and Taylor.
Fri, 23 Sep 2005 22:58:50 +0200 webertj new sat tactic imports resolution proofs from zChaff
Fri, 23 Sep 2005 22:21:50 +0200 wenzelm tuned order of targets;
Wed, 21 Sep 2005 11:50:20 +0200 wenzelm HOL-Complex-Matrix: fixed deps;
Tue, 20 Sep 2005 14:17:31 +0200 wenzelm HOL-ex: Library/Commutative_Ring.thy;
Tue, 20 Sep 2005 14:13:20 +0200 wenzelm moved Tools/comm_ring.ML to Library;
Tue, 20 Sep 2005 13:58:58 +0200 wenzelm removed Commutative_Ring.thy, added HOL/ex/Chinese.thy;
Mon, 19 Sep 2005 19:49:09 +0200 obua Removed superfluous HOL/Matrix/cplex/ROOT.ML.
Mon, 19 Sep 2005 18:30:22 +0200 paulson further simplification of the Isabelle-ATP linkup
Mon, 19 Sep 2005 15:12:13 +0200 paulson simplification of the Isabelle-ATP code; hooks for batch generation of problems
Sat, 17 Sep 2005 18:11:20 +0200 wenzelm generate: added HOL-Complex-Generate-HOLLight;
Thu, 15 Sep 2005 23:53:33 +0200 huffman merge Hyperreal/Transfer.thy and Hyperreal/StarType.thy into Hyperreal/StarDef.thy
less more (0) -300 -100 -60 tip