| Fri, 13 May 2011 23:24:06 +0200 |
wenzelm |
make ZF_cs snapshot after final setup;
|
file |
diff |
annotate
|
| Fri, 22 Apr 2011 13:58:13 +0200 |
wenzelm |
modernized Quantifier1 simproc setup;
|
file |
diff |
annotate
|
| Mon, 20 Dec 2010 16:44:33 +0100 |
wenzelm |
proper identifiers for consts and types;
|
file |
diff |
annotate
|
| Thu, 28 Oct 2010 23:19:52 +0200 |
wenzelm |
discontinued obsolete ML antiquotation @{theory_ref};
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Wed, 18 Aug 2010 12:08:21 +0200 |
haftmann |
more antiquotations
|
file |
diff |
annotate
|
| Thu, 29 Apr 2010 22:56:32 +0200 |
wenzelm |
proper context for mksimps etc. -- via simpset of the running Simplifier;
|
file |
diff |
annotate
|
| Sat, 13 Mar 2010 16:44:12 +0100 |
wenzelm |
removed old CVS Ids;
|
file |
diff |
annotate
|
| Sun, 28 Feb 2010 22:30:51 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Thu, 15 Oct 2009 23:28:10 +0200 |
wenzelm |
replaced String.concat by implode;
|
file |
diff |
annotate
|
| Sat, 29 Mar 2008 22:56:01 +0100 |
wenzelm |
functional theory setup -- requires linear access;
|
file |
diff |
annotate
|
| Sun, 07 Oct 2007 21:19:31 +0200 |
wenzelm |
modernized specifications;
|
file |
diff |
annotate
|
| Wed, 03 Oct 2007 22:33:17 +0200 |
wenzelm |
avoid unnamed infixes;
|
file |
diff |
annotate
|
| Sat, 21 Jan 2006 23:02:28 +0100 |
wenzelm |
removed duplicate type_solver (cf. Tools/typechk.ML);
|
file |
diff |
annotate
|
| Thu, 01 Dec 2005 22:03:01 +0100 |
wenzelm |
unfold_tac: static evaluation of simpset;
|
file |
diff |
annotate
|
| Mon, 17 Oct 2005 23:10:13 +0200 |
wenzelm |
change_claset/simpset;
|
file |
diff |
annotate
|
| Mon, 12 Sep 2005 18:20:32 +0200 |
haftmann |
introduced new-style AList operations
|
file |
diff |
annotate
|
| Tue, 02 Aug 2005 19:47:12 +0200 |
wenzelm |
simprocs: Simplifier.inherit_bounds;
|
file |
diff |
annotate
|
| Thu, 03 Mar 2005 12:43:01 +0100 |
skalberg |
Move towards standard functions.
|
file |
diff |
annotate
|
| Sun, 13 Feb 2005 17:15:14 +0100 |
skalberg |
Deleted Library.option type.
|
file |
diff |
annotate
|
| Fri, 30 Jul 2004 10:44:42 +0200 |
wenzelm |
keep type_solver;
|
file |
diff |
annotate
|
| Wed, 15 Jan 2003 16:45:32 +0100 |
paulson |
more new-style theories
|
file |
diff |
annotate
|
| Tue, 06 Aug 2002 11:22:05 +0200 |
wenzelm |
sane interface for simprocs;
|
file |
diff |
annotate
|
| Mon, 21 Jan 2002 14:47:55 +0100 |
paulson |
new simprules and classical rules
|
file |
diff |
annotate
|
| Sat, 12 Jan 2002 16:37:58 +0100 |
wenzelm |
renamed forall_elim_vars_safe to gen_all;
|
file |
diff |
annotate
|
| Fri, 11 Jan 2002 14:53:30 +0100 |
wenzelm |
replace gen_all by forall_elim_vars_safe;
|
file |
diff |
annotate
|
| Wed, 19 Dec 2001 11:13:27 +0100 |
paulson |
separation of the AC part of Main into Main_ZFC, plus a few new lemmas
|
file |
diff |
annotate
|
| Wed, 12 Dec 2001 20:37:31 +0100 |
wenzelm |
isatool expandshort;
|
file |
diff |
annotate
|
| Thu, 15 Nov 2001 18:21:38 +0100 |
wenzelm |
type_solver_tac: use TCSET' to refer to context of goal state (does
|
file |
diff |
annotate
|
| Thu, 15 Nov 2001 17:59:56 +0100 |
paulson |
miniscoping of UN and INT
|
file |
diff |
annotate
|
| Fri, 05 Oct 2001 21:37:33 +0200 |
wenzelm |
sane spacing of "-";
|
file |
diff |
annotate
|
| Mon, 21 May 2001 14:53:30 +0200 |
paulson |
if_splits and split_if_asm
|
file |
diff |
annotate
|
| Fri, 30 Mar 2001 12:31:10 +0200 |
paulson |
the one-point rule for bounded quantifiers
|
file |
diff |
annotate
|
| Thu, 07 Sep 2000 21:12:49 +0200 |
wenzelm |
tuned ML code (the_context, bind_thms(s));
|
file |
diff |
annotate
|
| Thu, 10 Aug 2000 11:27:34 +0200 |
paulson |
installation of cancellation simprocs for the integers
|
file |
diff |
annotate
|
| Tue, 21 Sep 1999 19:11:07 +0200 |
nipkow |
Mod because of new solver interface.
|
file |
diff |
annotate
|
| Wed, 27 Jan 1999 10:31:31 +0100 |
paulson |
new typechecking solver for the simplifier
|
file |
diff |
annotate
|
| Thu, 24 Sep 1998 17:17:14 +0200 |
oheimb |
renamed mk_meta_eq to mk_eq
|
file |
diff |
annotate
|
| Mon, 17 Aug 1998 13:09:08 +0200 |
paulson |
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
|
file |
diff |
annotate
|
| Mon, 27 Jul 1998 16:04:20 +0200 |
paulson |
A few new lemmas by Mark Staples
|
file |
diff |
annotate
|
| Mon, 13 Jul 1998 16:43:57 +0200 |
paulson |
Huge tidy-up: removal of leading \!\!
|
file |
diff |
annotate
|
| Mon, 03 Nov 1997 12:24:13 +0100 |
wenzelm |
isatool fixclasimp;
|
file |
diff |
annotate
|
| Tue, 14 Oct 1997 12:41:11 +0200 |
nipkow |
Added neagtion rules for Ball and Bex.
|
file |
diff |
annotate
|
| Fri, 10 Oct 1997 18:23:31 +0200 |
wenzelm |
fixed dots;
|
file |
diff |
annotate
|
| Fri, 06 Jun 1997 12:48:21 +0200 |
paulson |
Better miniscoping for bounded quantifiers
|
file |
diff |
annotate
|
| Wed, 02 Apr 1997 15:37:35 +0200 |
paulson |
Uses ZF.thy again, to make that theory usable
|
file |
diff |
annotate
|
| Thu, 09 Jan 1997 10:20:03 +0100 |
paulson |
Removal of needless "addIs [equality]", etc.
|
file |
diff |
annotate
|
| Tue, 07 Jan 1997 12:37:07 +0100 |
paulson |
Default rewrite rules for quantification over Collect(A,P)
|
file |
diff |
annotate
|
| Fri, 03 Jan 1997 15:01:55 +0100 |
paulson |
Implicit simpsets and clasets for FOL and ZF
|
file |
diff |
annotate
|
| Fri, 07 Jun 1996 10:56:37 +0200 |
paulson |
Addition of converse_iff, domain_converse, range_converse as rewrites
|
file |
diff |
annotate
|
| Tue, 26 Mar 1996 11:58:59 +0100 |
paulson |
Added new rewrite rules about cons and succ
|
file |
diff |
annotate
|
| Tue, 30 Jan 1996 13:42:57 +0100 |
clasohm |
expanded tabs
|
file |
diff |
annotate
|
| Thu, 13 Apr 1995 11:38:48 +0200 |
lcp |
Recoded function atomize so that new ways of creating
|
file |
diff |
annotate
|
| Thu, 12 Jan 1995 03:03:07 +0100 |
lcp |
Added singleton_iff, Sigma_empty1, Sigma_empty2, Collect_simps
|
file |
diff |
annotate
|
| Thu, 08 Dec 1994 11:28:34 +0100 |
lcp |
test_assume_tac: now tries eq_assume_tac on exceptional cases
|
file |
diff |
annotate
|
| Tue, 16 Aug 1994 19:01:26 +0200 |
lcp |
ZF/pair.ML: moved some definitions here from simpdata.ML
|
file |
diff |
annotate
|
| Fri, 12 Aug 1994 12:51:34 +0200 |
lcp |
installation of new inductive/datatype sections
|
file |
diff |
annotate
|
| Tue, 26 Jul 1994 13:44:42 +0200 |
lcp |
Axiom of choice, cardinality results, etc.
|
file |
diff |
annotate
|
| Tue, 12 Jul 1994 18:05:03 +0200 |
lcp |
new cardinal arithmetic developments
|
file |
diff |
annotate
|
| Tue, 21 Jun 1994 17:20:34 +0200 |
lcp |
Addition of cardinals and order types, various tidying
|
file |
diff |
annotate
|