Mercurial Mercurial > repos > isabelle / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) -100 -60 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Main.thy
Fri, 07 Nov 2014 11:28:37 +0100 traytel more complete fp_sugars for sum and prod; file | diff | annotate
Sun, 02 Nov 2014 18:21:45 +0100 wenzelm modernized header uniformly as section; file | diff | annotate
Thu, 23 Oct 2014 19:40:39 +0200 haftmann further downshift of theory Parity in the hierarchy file | diff | annotate
Thu, 23 Oct 2014 14:04:05 +0200 haftmann downshift of theory Parity in the hierarchy file | diff | annotate
Tue, 07 Oct 2014 23:29:43 +0200 wenzelm more bibtex entries; file | diff | annotate
Thu, 18 Sep 2014 16:47:40 +0200 blanchet moved old 'size' generator together with 'old_datatype' file | diff | annotate
Thu, 18 Sep 2014 16:47:40 +0200 blanchet moved 'old_datatype' out of 'Main' (but put it in 'HOL-Proofs' because of the inductive realizer) file | diff | annotate
Tue, 16 Sep 2014 19:23:37 +0200 blanchet tuned fact visibility file | diff | annotate
Tue, 16 Sep 2014 19:23:37 +0200 blanchet register 'prod' and 'sum' as datatypes, to allow N2M through them file | diff | annotate
Wed, 03 Sep 2014 00:06:26 +0200 blanchet tuned imports file | diff | annotate
Wed, 03 Sep 2014 00:06:24 +0200 blanchet use 'datatype_new' in 'Main' file | diff | annotate
Mon, 01 Sep 2014 16:34:40 +0200 blanchet renamed BNF theories file | diff | annotate
Thu, 28 Aug 2014 00:40:37 +0200 blanchet moved old 'smt' method out of 'Main' file | diff | annotate
Thu, 24 Jul 2014 11:54:15 +0200 wenzelm more robust notation BNF_Def.convol, which is private to main HOL, but may cause syntax ambiguities nonetheless (e.g. List.thy); file | diff | annotate
Wed, 11 Jun 2014 11:28:46 +0200 blanchet removed old SMT module from Sledgehammer file | diff | annotate
Fri, 21 Mar 2014 08:13:23 +0100 traytel simplified internal datatype construction file | diff | annotate
Tue, 11 Mar 2014 17:18:41 +0100 blanchet moved 'Quickcheck_Narrowing' further down the theory graph file | diff | annotate
Wed, 19 Feb 2014 10:30:21 +0100 traytel reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes file | diff | annotate
Mon, 17 Feb 2014 13:31:42 +0100 blanchet renamed old 'primrec' to 'old_primrec' (until the new 'primrec' can be moved above 'Nat' in the theory dependencies) file | diff | annotate
Thu, 23 Jan 2014 19:02:22 +0100 blanchet hide 'csum' etc. file | diff | annotate
Mon, 20 Jan 2014 22:24:48 +0100 blanchet renamed 'regular' to 'regularCard' to avoid clashes (e.g. in Meson_Test) file | diff | annotate
Mon, 20 Jan 2014 21:45:08 +0100 blanchet hide BNF notation file | diff | annotate
Mon, 20 Jan 2014 19:05:25 +0100 blanchet removed dependency of BNF package on Nitpick file | diff | annotate
Mon, 20 Jan 2014 18:59:53 +0100 blanchet deactivate one more cardinal notation file | diff | annotate
Mon, 20 Jan 2014 18:24:56 +0100 blanchet moved hide_const from BNF to Main file | diff | annotate
Mon, 20 Jan 2014 18:24:56 +0100 blanchet tuned names file | diff | annotate
Mon, 20 Jan 2014 18:24:56 +0100 blanchet tuning file | diff | annotate
Mon, 20 Jan 2014 18:24:56 +0100 blanchet compile file | diff | annotate
Mon, 20 Jan 2014 18:24:56 +0100 blanchet made BNF compile after move to HOL file | diff | annotate
Mon, 20 Jan 2014 18:24:56 +0100 blanchet moved BNF files to 'HOL' file | diff | annotate
Mon, 20 Jan 2014 18:24:55 +0100 blanchet kill notations file | diff | annotate
Mon, 20 Jan 2014 18:24:55 +0100 blanchet renamed '_FP' files to 'BNF_' files file | diff | annotate
Mon, 20 Jan 2014 18:24:55 +0100 blanchet moved subset of 'HOL-Cardinals' needed for BNF into 'HOL' file | diff | annotate
Thu, 16 Jan 2014 16:33:19 +0100 blanchet moved 'Zorn' into 'Main', since it's a BNF dependency file | diff | annotate
Thu, 21 Nov 2013 21:33:34 +0100 blanchet moving 'Order_Relation' to 'HOL' (since it's a BNF dependency) file | diff | annotate
Wed, 20 Nov 2013 20:45:20 +0100 blanchet moved 'coinduction' proof method to 'HOL' file | diff | annotate
Wed, 20 Nov 2013 18:58:00 +0100 blanchet factor 'List_Prefix' out of 'Sublist' and move to 'Main' (needed for codatatypes) file | diff | annotate
Tue, 13 Aug 2013 15:59:22 +0200 kuncar move Lifting/Transfer relevant parts of Library/Quotient_* to Main file | diff | annotate
Thu, 14 Feb 2013 12:24:42 +0100 haftmann abandoned theory Plain file | diff | annotate
Sat, 07 Jan 2012 20:18:56 +0100 haftmann dropped theory More_Set file | diff | annotate
Mon, 26 Dec 2011 22:17:10 +0100 haftmann incorporated More_Set and More_List into the Main body -- to be consolidated later file | diff | annotate
Tue, 13 Sep 2011 16:21:48 +0200 noschinl tune simpset for Complete_Lattices file | diff | annotate
Sat, 10 Sep 2011 10:29:24 +0200 haftmann renamed theory Complete_Lattice to Complete_Lattices, in accordance with Lattices, Orderings etc. file | diff | annotate
Sat, 20 Aug 2011 01:33:58 +0200 haftmann compatibility layer file | diff | annotate
Thu, 05 May 2011 10:47:31 +0200 bulwahn adding creation of exhaustive generators for records; simplifying dependencies in Main theory file | diff | annotate
Fri, 11 Mar 2011 15:21:13 +0100 bulwahn correcting dependencies after renaming file | diff | annotate
Mon, 08 Nov 2010 09:25:43 +0100 bulwahn adding code and theory for smallvalue generators, but do not setup the interpretation yet file | diff | annotate
Tue, 26 Oct 2010 13:16:43 +0200 blanchet integrated "smt" proof method with Sledgehammer file | diff | annotate
Tue, 26 Oct 2010 12:17:19 +0200 blanchet reverted e7a80c6752c9 -- there's not much point in putting a diagnosis tool (as opposed to a proof method) in Plain, but more importantly Sledgehammer must be in Main to use SMT solvers file | diff | annotate
Mon, 25 Oct 2010 13:34:57 +0200 haftmann moved sledgehammer to Plain; tuned dependencies file | diff | annotate
Thu, 12 Aug 2010 17:56:41 +0200 haftmann group record-related ML files file | diff | annotate
Wed, 12 May 2010 23:54:04 +0200 boehmes layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable file | diff | annotate
Mon, 22 Feb 2010 19:31:00 +0100 blanchet enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit file | diff | annotate
Fri, 19 Feb 2010 13:54:19 +0100 Cezary Kaliszyk Initial version of HOL quotient package. file | diff | annotate
Thu, 14 Jan 2010 15:06:38 +0100 blanchet reorder Quickcheck and Nitpick, so that Quickcheck gets loaded first and Auto-Quickcheck runs first (since it takes less time) file | diff | annotate
Thu, 29 Oct 2009 12:29:31 +0100 blanchet readded Predicate_Compile to Main file | diff | annotate
Wed, 28 Oct 2009 18:09:30 +0100 blanchet merged my Auto Nitpick change with Lukas's Predicate Compiler changes file | diff | annotate
Wed, 28 Oct 2009 17:43:43 +0100 blanchet introduced Auto Nitpick in addition to Auto Quickcheck; file | diff | annotate
Tue, 27 Oct 2009 09:02:22 +0100 bulwahn including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck file | diff | annotate
Thu, 22 Oct 2009 14:51:47 +0200 blanchet added Nitpick's theory and ML files to Isabelle/HOL; file | diff | annotate
less more (0) -100 -60 tip
isabelle