src/HOL/IsaMakefile
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
Sat, 03 Mar 2012 23:42:56 +0100 haftmann added actual dependencies
Sat, 03 Mar 2012 22:38:33 +0100 haftmann switch of target Import-HOL_Light-Imported: not operative at the moment
Sat, 03 Mar 2012 21:42:41 +0100 haftmann formal infrastructure for import sessions
Mon, 27 Feb 2012 23:30:38 +0100 wenzelm removed dead code (cf. a34d89ce6097);
Mon, 27 Feb 2012 12:12:28 +0100 wenzelm reactivated Find_Unused_Assms_Examples to avoid untested / dead stuff in the repository;
Fri, 24 Feb 2012 22:46:44 +0100 haftmann moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
Fri, 24 Feb 2012 19:45:10 +0100 wenzelm more precise clean target;
Fri, 24 Feb 2012 11:23:34 +0100 blanchet renamed 'try_methods' to 'try0'
Fri, 24 Feb 2012 09:40:02 +0100 haftmann given up disfruitful branch
Thu, 23 Feb 2012 21:25:59 +0100 haftmann moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
Wed, 22 Feb 2012 18:08:27 +0100 bulwahn NEWS
Wed, 22 Feb 2012 17:25:35 +0100 bulwahn adding some examples with find_unused_assms command
Wed, 22 Feb 2012 08:01:41 +0100 bulwahn moving Quickcheck's example to its own session
Tue, 21 Feb 2012 09:17:53 +0100 huffman renamed ex/Numeral.thy to ex/Numeral_Representation.thy
Thu, 02 Feb 2012 10:12:11 +0100 bulwahn adding an example for a datatype refinement which would allow rtrancl to be executable on an infinite type
Mon, 23 Jan 2012 17:40:32 +0100 blanchet added problem importer
Mon, 23 Jan 2012 17:40:32 +0100 blanchet renamed theory exporter
Mon, 23 Jan 2012 17:40:32 +0100 blanchet renamed two files to make room for a new file
Mon, 23 Jan 2012 17:40:31 +0100 blanchet rebranded Nitrox, for more uniformity
Tue, 17 Jan 2012 10:45:42 +0100 bulwahn renaming theory AList_Impl back to AList (reverting 1fec5b365f9b; AList with distinct key invariant is called DAList)
Tue, 17 Jan 2012 09:38:30 +0100 bulwahn renamed theory AList to DAList
Mon, 16 Jan 2012 07:46:58 +0100 nipkow missing dependency
Tue, 10 Jan 2012 10:17:07 +0100 bulwahn adding theory association lists with invariant
Sat, 07 Jan 2012 20:18:56 +0100 haftmann dropped theory More_Set
Fri, 06 Jan 2012 20:39:50 +0100 haftmann farewell to theory More_List
Mon, 26 Dec 2011 22:17:10 +0100 haftmann incorporated More_Set and More_List into the Main body -- to be consolidated later
Mon, 26 Dec 2011 17:40:43 +0100 haftmann dropped Executable_Set wrapper theory
Sat, 17 Dec 2011 12:42:10 +0100 wenzelm clarified modules that contribute to datatype package;
Fri, 16 Dec 2011 10:52:35 +0100 wenzelm clarified modules that contribute to datatype package;
Thu, 15 Dec 2011 17:37:14 +0100 wenzelm separate rep_datatype.ML;
Thu, 15 Dec 2011 09:13:32 +0100 nipkow merged
Thu, 15 Dec 2011 09:13:23 +0100 nipkow tuned
Wed, 14 Dec 2011 18:07:32 +0100 blanchet added new proof redirection code
Wed, 14 Dec 2011 16:30:32 +0100 bulwahn correcting dependencies after renaming
less more (0) -1000 -300 -100 -60 tip