src/HOL/Main.thy
Tue, 21 Sep 2021 11:34:58 +0200 wenzelm more uniform syntax;
Tue, 21 Sep 2021 00:20:47 +0200 wenzelm bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax;
Mon, 02 Aug 2021 13:30:56 +0200 wenzelm removed junk;
Mon, 02 Aug 2021 10:01:06 +0000 haftmann moved theory Bit_Operations into Main corpus
Fri, 14 May 2021 21:32:11 +0200 wenzelm reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
Fri, 14 Jun 2019 08:34:27 +0000 haftmann dropped former legacy input abbreviations
Sun, 07 Apr 2019 08:26:57 +0200 traytel bundle for cardinal syntax
Mon, 28 Jan 2019 10:27:47 +0100 nipkow more canonical and less specialized syntax
Sat, 10 Nov 2018 07:57:19 +0000 haftmann clarified status of legacy input abbreviations
Wed, 12 Sep 2018 18:44:31 +0200 nipkow added spaces because otherwise nonatomic arguments look awful: BIGf x -> BIG f x
Tue, 09 Jan 2018 15:18:41 +0100 wenzelm removed duplicate text;
Tue, 31 Oct 2017 07:11:03 +0000 haftmann removed ancient nat-int transfer
Sun, 08 Oct 2017 22:28:22 +0200 haftmann euclidean rings need no normalization
Fri, 08 Sep 2017 00:01:36 +0200 blanchet moved Nunchaku to Main; the goal is to move Nitpick out in the next 1-2 years
Sun, 14 May 2017 12:06:52 +0200 wenzelm obsolete (see also bdd17b18e103, f533820e7248);
Fri, 12 May 2017 20:03:50 +0200 haftmann relaxed theory dependencies
Sun, 23 Apr 2017 14:15:09 +0200 wenzelm added missing file (amending f533820e7248);
Wed, 10 Aug 2016 22:34:14 +0200 wenzelm simplified theory hierarchy;
Fri, 17 Jun 2016 09:44:16 +0200 hoelzl move Conditional_Complete_Lattices to Main
Sat, 09 Apr 2016 12:36:25 +0200 wenzelm old;
Mon, 28 Dec 2015 21:47:32 +0100 wenzelm former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
Sat, 18 Jul 2015 22:58:50 +0200 wenzelm isabelle update_cartouches;
Sun, 12 Apr 2015 11:33:19 +0200 hoelzl move filters to their own theory
Fri, 07 Nov 2014 11:28:37 +0100 traytel more complete fp_sugars for sum and prod;
Sun, 02 Nov 2014 18:21:45 +0100 wenzelm modernized header uniformly as section;
Thu, 23 Oct 2014 19:40:39 +0200 haftmann further downshift of theory Parity in the hierarchy
Thu, 23 Oct 2014 14:04:05 +0200 haftmann downshift of theory Parity in the hierarchy
Tue, 07 Oct 2014 23:29:43 +0200 wenzelm more bibtex entries;
Thu, 18 Sep 2014 16:47:40 +0200 blanchet moved old 'size' generator together with 'old_datatype'
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)
Tue, 16 Sep 2014 19:23:37 +0200 blanchet tuned fact visibility
Tue, 16 Sep 2014 19:23:37 +0200 blanchet register 'prod' and 'sum' as datatypes, to allow N2M through them
Wed, 03 Sep 2014 00:06:26 +0200 blanchet tuned imports
Wed, 03 Sep 2014 00:06:24 +0200 blanchet use 'datatype_new' in 'Main'
Mon, 01 Sep 2014 16:34:40 +0200 blanchet renamed BNF theories
Thu, 28 Aug 2014 00:40:37 +0200 blanchet moved old 'smt' method out of 'Main'
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);
Wed, 11 Jun 2014 11:28:46 +0200 blanchet removed old SMT module from Sledgehammer
Fri, 21 Mar 2014 08:13:23 +0100 traytel simplified internal datatype construction
Tue, 11 Mar 2014 17:18:41 +0100 blanchet moved 'Quickcheck_Narrowing' further down the theory graph
Wed, 19 Feb 2014 10:30:21 +0100 traytel reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
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)
Thu, 23 Jan 2014 19:02:22 +0100 blanchet hide 'csum' etc.
Mon, 20 Jan 2014 22:24:48 +0100 blanchet renamed 'regular' to 'regularCard' to avoid clashes (e.g. in Meson_Test)
Mon, 20 Jan 2014 21:45:08 +0100 blanchet hide BNF notation
Mon, 20 Jan 2014 19:05:25 +0100 blanchet removed dependency of BNF package on Nitpick
Mon, 20 Jan 2014 18:59:53 +0100 blanchet deactivate one more cardinal notation
Mon, 20 Jan 2014 18:24:56 +0100 blanchet moved hide_const from BNF to Main
Mon, 20 Jan 2014 18:24:56 +0100 blanchet tuned names
Mon, 20 Jan 2014 18:24:56 +0100 blanchet tuning
Mon, 20 Jan 2014 18:24:56 +0100 blanchet compile
Mon, 20 Jan 2014 18:24:56 +0100 blanchet made BNF compile after move to HOL
Mon, 20 Jan 2014 18:24:56 +0100 blanchet moved BNF files to 'HOL'
Mon, 20 Jan 2014 18:24:55 +0100 blanchet kill notations
Mon, 20 Jan 2014 18:24:55 +0100 blanchet renamed '_FP' files to 'BNF_' files
Mon, 20 Jan 2014 18:24:55 +0100 blanchet moved subset of 'HOL-Cardinals' needed for BNF into 'HOL'
Thu, 16 Jan 2014 16:33:19 +0100 blanchet moved 'Zorn' into 'Main', since it's a BNF dependency
Thu, 21 Nov 2013 21:33:34 +0100 blanchet moving 'Order_Relation' to 'HOL' (since it's a BNF dependency)
Wed, 20 Nov 2013 20:45:20 +0100 blanchet moved 'coinduction' proof method to 'HOL'
Wed, 20 Nov 2013 18:58:00 +0100 blanchet factor 'List_Prefix' out of 'Sublist' and move to 'Main' (needed for codatatypes)
Tue, 13 Aug 2013 15:59:22 +0200 kuncar move Lifting/Transfer relevant parts of Library/Quotient_* to Main
Thu, 14 Feb 2013 12:24:42 +0100 haftmann abandoned theory Plain
Sat, 07 Jan 2012 20:18:56 +0100 haftmann dropped theory More_Set
Mon, 26 Dec 2011 22:17:10 +0100 haftmann incorporated More_Set and More_List into the Main body -- to be consolidated later
Tue, 13 Sep 2011 16:21:48 +0200 noschinl tune simpset for Complete_Lattices
Sat, 10 Sep 2011 10:29:24 +0200 haftmann renamed theory Complete_Lattice to Complete_Lattices, in accordance with Lattices, Orderings etc.
Sat, 20 Aug 2011 01:33:58 +0200 haftmann compatibility layer
Thu, 05 May 2011 10:47:31 +0200 bulwahn adding creation of exhaustive generators for records; simplifying dependencies in Main theory
Fri, 11 Mar 2011 15:21:13 +0100 bulwahn correcting dependencies after renaming
Mon, 08 Nov 2010 09:25:43 +0100 bulwahn adding code and theory for smallvalue generators, but do not setup the interpretation yet
Tue, 26 Oct 2010 13:16:43 +0200 blanchet integrated "smt" proof method with Sledgehammer
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
Mon, 25 Oct 2010 13:34:57 +0200 haftmann moved sledgehammer to Plain; tuned dependencies
Thu, 12 Aug 2010 17:56:41 +0200 haftmann group record-related ML files
Wed, 12 May 2010 23:54:04 +0200 boehmes layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
Mon, 22 Feb 2010 19:31:00 +0100 blanchet enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
Fri, 19 Feb 2010 13:54:19 +0100 Cezary Kaliszyk Initial version of HOL quotient package.
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)
Thu, 29 Oct 2009 12:29:31 +0100 blanchet readded Predicate_Compile to Main
Wed, 28 Oct 2009 18:09:30 +0100 blanchet merged my Auto Nitpick change with Lukas's Predicate Compiler changes
Wed, 28 Oct 2009 17:43:43 +0100 blanchet introduced Auto Nitpick in addition to Auto Quickcheck;
Tue, 27 Oct 2009 09:02:22 +0100 bulwahn including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
Thu, 22 Oct 2009 14:51:47 +0200 blanchet added Nitpick's theory and ML files to Isabelle/HOL;
Tue, 19 May 2009 13:57:32 +0200 haftmann moved Code_Index, Random and Quickcheck before Main
Fri, 13 Feb 2009 09:54:47 +0100 nipkow Moved Nat_Int_Bij into Library
Fri, 06 Feb 2009 13:43:19 +0100 blanchet Rearrange Refute/SAT theory dependencies so as to use even more antiquotations in refute.ML +
Fri, 02 Jan 2009 00:21:59 +0100 wenzelm tuned header and description of boot files;
Wed, 17 Sep 2008 21:27:14 +0200 wenzelm moved global ML bindings to global place;
Tue, 16 Sep 2008 09:21:24 +0200 haftmann evaluation using code generator
Tue, 02 Sep 2008 21:31:28 +0200 nipkow Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
Thu, 26 Jun 2008 10:06:54 +0200 haftmann added dummy citiation
Tue, 22 Apr 2008 08:33:10 +0200 haftmann dropped theory PreList
Fri, 25 Jan 2008 14:53:58 +0100 haftmann consistent interacitve bootstrap of HOL-Main
Mon, 29 Oct 2007 16:13:41 +0100 wenzelm qualified Proofterm.proofs;
Thu, 27 Sep 2007 17:55:28 +0200 paulson removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
Tue, 25 Sep 2007 12:16:08 +0200 haftmann datatype interpretators for size and datatype_realizer
Wed, 19 Sep 2007 12:17:13 +0200 berghofe Enclosed end_theory in text antiquotation to make LaTeX happy.
Tue, 18 Sep 2007 17:53:37 +0200 paulson metis now available in PreList
Thu, 31 May 2007 18:16:54 +0200 wenzelm HOL_proofs;
Sun, 06 May 2007 21:49:26 +0200 haftmann minimal import
Wed, 08 Nov 2006 21:45:15 +0100 wenzelm incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
Fri, 25 Aug 2006 18:44:59 +0200 paulson replaced skolem declarations by automatic skolemization of everything
Tue, 08 Aug 2006 18:40:56 +0200 paulson skolem declarations for built-in theorems
Wed, 10 May 2006 16:23:21 +0200 wenzelm revert accidental text change;
Tue, 09 May 2006 14:18:40 +0200 haftmann introduced characters for code generator; some improved code lemmas for some list functions
Fri, 23 Dec 2005 17:37:54 +0100 paulson the "skolem" attribute and better initialization of the clause database
Thu, 01 Dec 2005 15:45:54 +0100 paulson restoring the old status of subset_refl
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").
Thu, 29 Sep 2005 15:50:44 +0200 wenzelm explicit dependencies of SAT vs. Refute;
Fri, 23 Sep 2005 22:58:50 +0200 webertj new sat tactic imports resolution proofs from zChaff
Fri, 23 Sep 2005 16:01:45 +0200 webertj header (title/ID) added
Fri, 23 Sep 2005 15:45:12 +0200 webertj typo fixed: rufute -> refute
Tue, 20 Sep 2005 14:03:38 +0200 wenzelm removed Commutative_Ring hacks;
Sat, 17 Sep 2005 18:11:21 +0200 wenzelm minor cleanup, moved stuff in its proper place;
Thu, 15 Sep 2005 17:45:17 +0200 paulson moving Commutative_Ring to the correct theory
Wed, 14 Sep 2005 23:14:58 +0200 wenzelm hide the rather generic names used in theory Commutative_Ring;
Wed, 14 Sep 2005 22:04:37 +0200 wenzelm imports Commutative_Ring;
Tue, 12 Jul 2005 11:51:31 +0200 berghofe Auxiliary functions to be used in generated code are now defined using "attach".
Fri, 01 Jul 2005 13:56:34 +0200 berghofe Moved some code lemmas from Main to Nat.
Tue, 28 Jun 2005 15:27:45 +0200 paulson Constant "If" is now local
less more (0) -120 tip