src/HOL/IsaMakefile
Tue, 24 Jul 2012 08:12:15 +0200 bulwahn moving Quickcheck_Examples back to test to run a minimal test even with the mira testing infrastructure
Tue, 24 Jul 2012 21:46:48 +0200 wenzelm reactivated HOL-NSA-Examples;
Sun, 22 Jul 2012 09:56:34 +0200 haftmann library theories for debugging and parallel computing using code generation towards Isabelle/ML
Fri, 20 Jul 2012 22:19:45 +0200 blanchet renamed ML files
Thu, 19 Jul 2012 19:38:39 +0200 haftmann removed ML module DSeq which was a part of the ancient code generator (cf. 58e33a125f32)
Wed, 18 Jul 2012 08:44:03 +0200 blanchet rationalize relevance filter, slowing moving code from Iter to MaSh
Wed, 18 Jul 2012 08:44:03 +0200 blanchet renaming
Wed, 11 Jul 2012 21:43:19 +0200 blanchet further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
Wed, 11 Jul 2012 13:59:39 +0200 bulwahn merged
Wed, 11 Jul 2012 13:54:37 +0200 bulwahn adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
Tue, 10 Jul 2012 23:36:03 +0200 blanchet moved MaSh into own files
Tue, 10 Jul 2012 18:41:34 +0200 bulwahn adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
Mon, 09 Jul 2012 10:04:07 +0200 bulwahn adding the hotel key card example in Quickcheck-Examples
Thu, 05 Jul 2012 13:24:09 +0200 haftmann Stub theory for division on functionals.
Mon, 02 Jul 2012 12:23:30 +0200 bulwahn adding some minimal documentation and an example of quickcheck's interfaces
Thu, 28 Jun 2012 09:14:57 +0200 Andreas Lochbihler add generic phantom type
Wed, 20 Jun 2012 16:54:08 +0200 Rafal Kolanski Integrated set comprehension pointfree simproc.
Fri, 01 Jun 2012 08:32:26 +0200 Andreas Lochbihler merged
Thu, 31 May 2012 16:58:38 +0200 Andreas Lochbihler unify Card_Univ and Cardinality
Mon, 28 May 2012 02:18:46 +0200 bulwahn adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
Wed, 30 May 2012 16:05:06 +0200 Andreas Lochbihler remove pretty syntax for FinFuns at the end and provide separate syntax theory
Tue, 29 May 2012 15:31:58 +0200 Andreas Lochbihler move FinFuns from AFP to repository
Fri, 18 May 2012 16:43:38 +0200 blanchet added a timeout to "try0" in Mirabelle
Fri, 27 Apr 2012 15:24:37 +0200 blanchet get rid of old CASC setup and move the arithmetic part to a new theory
Fri, 27 Apr 2012 15:24:37 +0200 blanchet move file to where it belongs
Tue, 24 Apr 2012 13:59:29 +0100 sultana reversed Tools to Actions Mirabelle renaming;
Mon, 23 Apr 2012 12:14:35 +0200 hoelzl reworked Probability theory
Sun, 22 Apr 2012 11:05:04 +0200 huffman new example theory for quotient/transfer
Sat, 21 Apr 2012 13:49:31 +0200 huffman new example theory for transfer package
Thu, 19 Apr 2012 20:19:13 +0200 nipkow added revised version of Abs_Int
Thu, 19 Apr 2012 17:32:30 +0200 nipkow reorganised IMP
Tue, 17 Apr 2012 16:21:47 +1000 Thomas Sewell New tactic "word_bitwise" expands word equalities/inequalities into logic.
Sat, 14 Apr 2012 23:52:17 +0100 sultana renamed mirabelle Tools directory to Actions, to make consistent with 'usage' description;
Sat, 14 Apr 2012 19:29:31 +0200 krauss removed HOL/ex/Set_Algebras -- outdated clone, obsolete as example
Tue, 03 Apr 2012 22:31:00 +0200 huffman new transfer proof method
Tue, 03 Apr 2012 22:04:50 +0200 huffman renamed Tools/transfer.ML to Tools/legacy_transfer.ML
Tue, 03 Apr 2012 20:56:32 +0200 huffman merged
Tue, 03 Apr 2012 15:15:00 +0200 huffman modernized obsolete old-style theory name with proper new-style underscore
Tue, 03 Apr 2012 17:48:16 +0200 wenzelm merged
Tue, 03 Apr 2012 16:26:48 +0200 kuncar new package Lifting - initial commit
Tue, 03 Apr 2012 16:53:32 +0200 wenzelm some context examples;
Sun, 01 Apr 2012 23:21:54 +0200 krauss merged, manually resolving conflicts due to session renaming (cf. 6488c5efec49)
Sun, 01 Apr 2012 22:41:56 +0200 krauss renamed import session back to Import, conforming to directory name; NEWS
Sun, 01 Apr 2012 23:07:15 +0200 wenzelm more precise IsaMakefile (eg. see HOL-Algebra);
Sun, 01 Apr 2012 22:14:59 +0200 krauss merged
Sun, 01 Apr 2012 22:03:45 +0200 krauss removed old HOL4 import -- corresponding exporter is lost, code is broken, no users known, maintenance nightmare
Sun, 01 Apr 2012 14:50:47 +0200 Cezary Kaliszyk Modernized HOL-Import for HOL Light
Sun, 01 Apr 2012 16:09:58 +0200 huffman removed Nat_Numeral.thy, moving all theorems elsewhere
Fri, 30 Mar 2012 18:56:02 +0200 haftmann dropped now obsolete Cset theories
Fri, 30 Mar 2012 14:27:29 +0200 huffman remove content-free theory ex/Arithmetic_Series_Complex.thy
Fri, 30 Mar 2012 08:44:01 +0200 bulwahn adding theory to prove completeness of the exhaustive generators
Mon, 26 Mar 2012 20:09:18 +0200 huffman revert changeset 500a5d97511a, re-enabling HOL-Proofs-Lambda
Mon, 26 Mar 2012 19:18:03 +0200 wenzelm disabled HOL-Proofs-Lambda temporarily, which causes problems with 2a1953f0d20d;
Sun, 25 Mar 2012 20:15:39 +0200 huffman merged fork with new numeral representation (see NEWS)
Sat, 17 Mar 2012 12:52:40 +0100 wenzelm renamed HOL-Matrix to HOL-Matrix_LP to avoid name clash with AFP;
Thu, 15 Mar 2012 22:20:07 +0100 wenzelm more precise TPTP keywords and dependencies;
Wed, 07 Mar 2012 14:30:35 +0100 wenzelm some recovery of IsaMakefile targets from f3c10e908f65;
Sun, 04 Mar 2012 10:34:44 +0100 haftmann move test targets to test target
Sun, 04 Mar 2012 10:33:47 +0100 haftmann dropped images for importer sessions
Sun, 04 Mar 2012 00:27:07 +0100 haftmann more accurate dependencies
less more (0) -1000 -300 -100 -60 tip