src/ZF/OrdQuant.thy
Sun, 24 May 2020 19:57:13 +0000 haftmann better closeup and more consistent terminology
Fri, 04 Jan 2019 23:22:53 +0100 wenzelm isabelle update -u control_cartouches;
Thu, 03 Jan 2019 21:15:52 +0100 wenzelm isabelle update -u mixfix_cartouches;
Sat, 10 Oct 2015 22:23:25 +0200 wenzelm tuned syntax -- more symbols;
Fri, 09 Oct 2015 20:26:03 +0200 wenzelm discontinued specific HTML syntax;
Tue, 28 Jul 2015 20:59:39 +0200 wenzelm more explicit context;
Thu, 23 Jul 2015 14:25:05 +0200 wenzelm isabelle update_cartouches;
Sat, 07 Mar 2015 21:32:31 +0100 wenzelm clarified Drule.gen_all: observe context more carefully;
Tue, 10 Feb 2015 14:48:26 +0100 wenzelm proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
Sun, 02 Nov 2014 16:39:54 +0100 wenzelm modernized header;
Sat, 01 Nov 2014 14:20:38 +0100 wenzelm eliminated spurious semicolons;
Sat, 22 Mar 2014 16:50:52 +0100 wenzelm more antiquotations;
Sun, 12 Jan 2014 14:32:22 +0100 wenzelm tuned signature;
Thu, 18 Apr 2013 17:07:01 +0200 wenzelm simplifier uses proper Proof.context instead of historic type simpset;
Thu, 15 Mar 2012 16:35:02 +0000 paulson replacing ":" by "\<in>"
Tue, 06 Mar 2012 15:15:49 +0000 paulson mathematical symbols instead of ASCII
Thu, 24 Nov 2011 21:01:06 +0100 wenzelm modernized some old-style infix operations, which were left over from the time of ML proof scripts;
Fri, 22 Apr 2011 15:05:04 +0200 wenzelm misc tuning and simplification;
Fri, 22 Apr 2011 14:30:32 +0200 wenzelm proper context for Quantifier1 simprocs (avoid bad ProofContext.init_global from abc655166d61);
Fri, 22 Apr 2011 13:58:13 +0200 wenzelm modernized Quantifier1 simproc setup;
Fri, 18 Feb 2011 16:22:27 +0100 wenzelm more precise headers;
Wed, 25 Aug 2010 18:36:22 +0200 wenzelm renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
Thu, 29 Apr 2010 22:56:32 +0200 wenzelm proper context for mksimps etc. -- via simpset of the running Simplifier;
Thu, 11 Feb 2010 22:06:37 +0100 wenzelm numeral syntax: clarify parse trees vs. actual terms;
Wed, 15 Jul 2009 23:48:21 +0200 wenzelm more antiquotations;
Wed, 17 Sep 2008 21:27:08 +0200 wenzelm back to dynamic the_context(), because static @{theory} is invalidated if ML environment changes within the same code block;
Sat, 29 Mar 2008 19:14:00 +0100 wenzelm replaced 'ML_setup' by 'ML';
Wed, 19 Mar 2008 22:47:35 +0100 wenzelm eliminated change_claset/simpset;
Sun, 07 Oct 2007 21:19:31 +0200 wenzelm modernized specifications;
Thu, 01 Dec 2005 22:03:01 +0100 wenzelm unfold_tac: static evaluation of simpset;
Mon, 17 Oct 2005 23:10:13 +0200 wenzelm change_claset/simpset;
Tue, 02 Aug 2005 19:47:12 +0200 wenzelm simprocs: Simplifier.inherit_bounds;
Fri, 17 Jun 2005 16:12:49 +0200 haftmann migrated theory headers to new format
Wed, 14 Apr 2004 14:13:05 +0200 kleing use more symbols in HTML output
Thu, 06 Feb 2003 11:01:05 +0100 paulson changed ** to ## to avoid conflict with new comment syntax
Tue, 01 Oct 2002 13:26:10 +0200 paulson Numerous cosmetic changes, prompted by the new simplifier
Tue, 06 Aug 2002 11:22:05 +0200 wenzelm sane interface for simprocs;
Tue, 16 Jul 2002 16:28:49 +0200 paulson tweaked definition of setclass
Wed, 10 Jul 2002 16:54:07 +0200 paulson Fixed quantified variable name preservation for ball and bex (bounded quants)
Fri, 05 Jul 2002 11:39:52 +0200 paulson fixed precedences of **
Thu, 04 Jul 2002 16:59:54 +0200 paulson Constructible: some separation axioms
Thu, 04 Jul 2002 10:50:24 +0200 paulson miniscoping for class-bounded quantifiers (rall and rex)
Fri, 28 Jun 2002 11:24:36 +0200 paulson added class quantifiers
Mon, 24 Jun 2002 11:59:14 +0200 paulson moving some results around
Thu, 23 May 2002 17:05:21 +0200 paulson new definition of "apply" and new simprule "beta_if"
Wed, 22 May 2002 19:34:01 +0200 paulson more tidying
Wed, 22 May 2002 18:11:57 +0200 paulson tidying up
Wed, 22 May 2002 17:25:40 +0200 paulson tidied
Tue, 21 May 2002 18:25:28 +0200 paulson conversion of OrdQuant.ML to Isar
Fri, 17 May 2002 16:54:25 +0200 paulson New theorems from Constructible, and moving some Isar material from Main
Wed, 15 May 2002 10:42:32 +0200 paulson better simplification of trivial existential equalities
Wed, 08 May 2002 10:12:57 +0200 paulson new lemmas
Mon, 21 Jan 2002 14:47:55 +0100 paulson new simprules and classical rules
Mon, 21 Jan 2002 11:25:45 +0100 paulson lexical tidying
Tue, 15 Jan 2002 10:24:20 +0100 paulson now [rule_format] knows about ospec
Tue, 08 Jan 2002 16:09:09 +0100 paulson Added some simprules proofs.
Thu, 03 Jan 2002 17:01:59 +0100 paulson Some new theorems for ordinals
Wed, 19 Dec 2001 11:13:27 +0100 paulson separation of the AC part of Main into Main_ZFC, plus a few new lemmas
Fri, 09 Nov 2001 00:09:47 +0100 wenzelm eliminated old "symbols" syntax, use "xsymbols" instead;
Tue, 12 Jan 1999 15:17:37 +0100 wenzelm eliminated global/local names;
less more (0) -60 tip