| Mon, 08 Mar 2021 09:11:09 +0100 |
\----- start update Isabelle2020 --> Isabelle2021
|
file | diff | annotate |
| Tue, 03 Sep 2019 16:10:31 +0200 |
\----- start update Isabelle2018 --> Isabelle2019
|
file | diff | annotate |
| Fri, 19 Jan 2018 12:49:17 +0100 |
\----- start update Isabelle2015 --> Isabelle2017
|
file | diff | annotate |
| Sat, 05 Dec 2015 16:09:41 +0100 |
switched from Isabelle2014 to Isabelle2015, intermediate state
|
file | diff | annotate |
| Sun, 12 Jan 2014 14:32:22 +0100 |
tuned signature;
|
file | diff | annotate |
| Thu, 18 Apr 2013 17:07:01 +0200 |
simplifier uses proper Proof.context instead of historic type simpset;
|
file | diff | annotate |
| Wed, 22 Aug 2012 22:55:41 +0200 |
prefer ML_file over old uses;
|
file | diff | annotate |
| Thu, 15 Mar 2012 16:35:02 +0000 |
replacing ":" by "\<in>"
|
file | diff | annotate |
| Thu, 08 Mar 2012 16:43:29 +0000 |
Structured and calculation-based proofs (with new trans rules!)
|
file | diff | annotate |
| Tue, 06 Mar 2012 16:06:52 +0000 |
Using mathematical notation for <-> and cardinal arithmetic
|
file | diff | annotate |
| Tue, 06 Mar 2012 15:15:49 +0000 |
mathematical symbols instead of ASCII
|
file | diff | annotate |
| Thu, 24 Nov 2011 21:01:06 +0100 |
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
|
file | diff | annotate |
| Wed, 23 Nov 2011 22:59:39 +0100 |
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
|
file | diff | annotate |
| Sun, 20 Nov 2011 20:15:02 +0100 |
eliminated obsolete "standard";
|
file | diff | annotate |
| Fri, 13 May 2011 23:58:40 +0200 |
clarified map_simpset versus Simplifier.map_simpset_global;
|
file | diff | annotate |
| Fri, 13 May 2011 23:24:06 +0200 |
make ZF_cs snapshot after final setup;
|
file | diff | annotate |
| Fri, 22 Apr 2011 15:05:04 +0200 |
misc tuning and simplification;
|
file | diff | annotate |
| Fri, 22 Apr 2011 14:30:32 +0200 |
proper context for Quantifier1 simprocs (avoid bad ProofContext.init_global from abc655166d61);
|
file | diff | annotate |
| Fri, 22 Apr 2011 13:58:13 +0200 |
modernized Quantifier1 simproc setup;
|
file | diff | annotate |
| Fri, 18 Feb 2011 16:22:27 +0100 |
more precise headers;
|
file | diff | annotate |
| Wed, 03 Dec 2008 15:58:44 +0100 |
made repository layout more coherent with logical distribution structure; stripped some $Id$s
|
file | diff | annotate |
| Sun, 07 Oct 2007 21:19:31 +0200 |
modernized specifications;
|
file | diff | annotate |
| Tue, 02 Aug 2005 19:47:11 +0200 |
tuned;
|
file | diff | annotate |
| Fri, 17 Jun 2005 16:12:49 +0200 |
migrated theory headers to new format
|
file | diff | annotate |
| Wed, 02 Jun 2004 17:35:08 +0200 |
new rules for simplifying quantifiers with Sigma
|
file | diff | annotate |
| Wed, 28 Aug 2002 13:08:50 +0200 |
various new lemmas for Constructible
|
file | diff | annotate |
| Sun, 14 Jul 2002 19:59:55 +0200 |
Removal of mono.thy
|
file | diff | annotate |
| Sun, 23 Jun 2002 10:14:13 +0200 |
conversion of Sum, pair to Isar script
|
file | diff | annotate |
| Fri, 05 Oct 2001 16:04:56 +0200 |
tuned;
|
file | diff | annotate |
| Thu, 10 Aug 2000 11:27:34 +0200 |
installation of cancellation simprocs for the integers
|
file | diff | annotate |
| Fri, 03 Jan 1997 15:01:55 +0100 |
Implicit simpsets and clasets for FOL and ZF
|
file | diff | annotate |
| Tue, 16 Nov 1993 14:24:21 +0100 |
made pseudo theories for all ML files;
|
file | diff | annotate |