| #
a4bab154 |
|
04-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
| #
34035ccd |
|
04-Mar-2015 |
wenzelm <none@none> |
tuned signature -- prefer qualified names;
|
| #
335dc010 |
|
13-May-2011 |
wenzelm <none@none> |
make ZF_cs snapshot after final setup;
|
| #
f1968c93 |
|
22-Apr-2011 |
wenzelm <none@none> |
modernized Quantifier1 simproc setup;
|
| #
f95e18b9 |
|
20-Dec-2010 |
wenzelm <none@none> |
proper identifiers for consts and types;
|
| #
ac23a361 |
|
28-Oct-2010 |
wenzelm <none@none> |
discontinued obsolete ML antiquotation @{theory_ref};
|
| #
2ab2e08e |
|
25-Aug-2010 |
wenzelm <none@none> |
renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
|
| #
b4ff8366 |
|
17-Aug-2010 |
haftmann <none@none> |
more antiquotations
|
| #
b96c5111 |
|
29-Apr-2010 |
wenzelm <none@none> |
proper context for mksimps etc. -- via simpset of the running Simplifier;
|
| #
458a4961 |
|
13-Mar-2010 |
wenzelm <none@none> |
removed old CVS Ids;
tuned headers;
|
| #
2b1723df |
|
28-Feb-2010 |
wenzelm <none@none> |
more antiquotations;
eliminated legacy ML bindings;
|
| #
75401f7b |
|
15-Oct-2009 |
wenzelm <none@none> |
replaced String.concat by implode;
replaced String.concatWith by space_implode;
replaced (Seq.flat o Seq.map) by Seq.maps;
replaced List.mapPartial by map_filter;
replaced List.concat by flat;
replaced (flat o map) by maps, which produces less garbage;
|
| #
ebb10abd |
|
29-Mar-2008 |
wenzelm <none@none> |
functional theory setup -- requires linear access;
|
| #
e7a16ceb |
|
07-Oct-2007 |
wenzelm <none@none> |
modernized specifications;
removed legacy ML bindings;
|
| #
3143a6c0 |
|
03-Oct-2007 |
wenzelm <none@none> |
avoid unnamed infixes;
|
| #
e6d5e676 |
|
21-Jan-2006 |
wenzelm <none@none> |
removed duplicate type_solver (cf. Tools/typechk.ML);
|
| #
dcc17ba3 |
|
01-Dec-2005 |
wenzelm <none@none> |
unfold_tac: static evaluation of simpset;
|
| #
3deee062 |
|
17-Oct-2005 |
wenzelm <none@none> |
change_claset/simpset;
|
| #
dcefbda4 |
|
12-Sep-2005 |
haftmann <none@none> |
introduced new-style AList operations
|
| #
593d5827 |
|
02-Aug-2005 |
wenzelm <none@none> |
simprocs: Simplifier.inherit_bounds;
|
| #
eee46a1e |
|
02-Mar-2005 |
skalberg <none@none> |
Move towards standard functions.
|
| #
3dffd254 |
|
13-Feb-2005 |
skalberg <none@none> |
Deleted Library.option type.
|
| #
c4b65375 |
|
30-Jul-2004 |
wenzelm <none@none> |
keep type_solver;
|
| #
d75e992b |
|
15-Jan-2003 |
paulson <none@none> |
more new-style theories
|
| #
1f05977e |
|
06-Aug-2002 |
wenzelm <none@none> |
sane interface for simprocs;
|
| #
28b04eed |
|
21-Jan-2002 |
paulson <none@none> |
new simprules and classical rules
|
| #
7e01175e |
|
12-Jan-2002 |
wenzelm <none@none> |
renamed forall_elim_vars_safe to gen_all;
|
| #
b8b69ab5 |
|
11-Jan-2002 |
wenzelm <none@none> |
replace gen_all by forall_elim_vars_safe;
|
| #
8bdf32a4 |
|
19-Dec-2001 |
paulson <none@none> |
separation of the AC part of Main into Main_ZFC, plus a few new lemmas
|
| #
afc254fb |
|
12-Dec-2001 |
wenzelm <none@none> |
isatool expandshort;
|
| #
253e96b8 |
|
15-Nov-2001 |
wenzelm <none@none> |
type_solver_tac: use TCSET' to refer to context of goal state (does
*not* work with local proof contexts of Isar / new-style locales);
|
| #
6b786961 |
|
15-Nov-2001 |
paulson <none@none> |
miniscoping of UN and INT
|
| #
e7a2d52e |
|
05-Oct-2001 |
wenzelm <none@none> |
sane spacing of "-";
|
| #
402d0364 |
|
21-May-2001 |
paulson <none@none> |
if_splits and split_if_asm
|
| #
ef843b83 |
|
29-Mar-2001 |
paulson <none@none> |
the one-point rule for bounded quantifiers
|
| #
aa223cf5 |
|
07-Sep-2000 |
wenzelm <none@none> |
tuned ML code (the_context, bind_thms(s));
|
| #
8e86760f |
|
10-Aug-2000 |
paulson <none@none> |
installation of cancellation simprocs for the integers
|
| #
3115c3d5 |
|
21-Sep-1999 |
nipkow <none@none> |
Mod because of new solver interface.
|
| #
dd096d87 |
|
27-Jan-1999 |
paulson <none@none> |
new typechecking solver for the simplifier
|
| #
47e59d2b |
|
24-Sep-1998 |
oheimb <none@none> |
renamed mk_meta_eq to mk_eq
|
| #
4fbe76b2 |
|
17-Aug-1998 |
paulson <none@none> |
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
contains fewer theorems than before
|
| #
103d6e70 |
|
27-Jul-1998 |
paulson <none@none> |
A few new lemmas by Mark Staples
|
| #
188b4622 |
|
13-Jul-1998 |
paulson <none@none> |
Huge tidy-up: removal of leading \!\!
addsplits split_tac[split_if] now default
nat_succI now included by default
|
| #
80fba2c0 |
|
02-Nov-1997 |
wenzelm <none@none> |
isatool fixclasimp;
|
| #
39785d1c |
|
13-Oct-1997 |
nipkow <none@none> |
Added neagtion rules for Ball and Bex.
ZF/AC now fails to build. Larry to fix.
|
| #
daf66f30 |
|
10-Oct-1997 |
wenzelm <none@none> |
fixed dots;
|
| #
5fd99d91 |
|
05-Jun-1997 |
paulson <none@none> |
Better miniscoping for bounded quantifiers
|
| #
147421eb |
|
02-Apr-1997 |
paulson <none@none> |
Uses ZF.thy again, to make that theory usable
|
| #
c176a95e |
|
09-Jan-1997 |
paulson <none@none> |
Removal of needless "addIs [equality]", etc.
|
| #
bd3a9558 |
|
06-Jan-1997 |
paulson <none@none> |
Default rewrite rules for quantification over Collect(A,P)
|
| #
f3f91f1c |
|
03-Jan-1997 |
paulson <none@none> |
Implicit simpsets and clasets for FOL and ZF
|
| #
d41a298a |
|
07-Jun-1996 |
paulson <none@none> |
Addition of converse_iff, domain_converse, range_converse as rewrites
|
| #
79d1c415 |
|
26-Mar-1996 |
paulson <none@none> |
Added new rewrite rules about cons and succ
|
| #
0fa32dcf |
|
30-Jan-1996 |
clasohm <none@none> |
expanded tabs
|
| #
71a8498a |
|
13-Apr-1995 |
lcp <none@none> |
Recoded function atomize so that new ways of creating
simplification rules can be added easily.
|
| #
432945da |
|
11-Jan-1995 |
lcp <none@none> |
Added singleton_iff, Sigma_empty1, Sigma_empty2, Collect_simps
and UnInt_simps to ZF_ss. Added consI1 to ZF_typechecks.
|
| #
7730fc1e |
|
08-Dec-1994 |
lcp <none@none> |
test_assume_tac: now tries eq_assume_tac on exceptional cases
(formulae not of the form a:?A). Affects typechk_tac.
|
| #
226c68b5 |
|
16-Aug-1994 |
lcp <none@none> |
ZF/pair.ML: moved some definitions here from simpdata.ML
|
| #
9df696ad |
|
11-Aug-1994 |
lcp <none@none> |
installation of new inductive/datatype sections
|
| #
199800bc |
|
26-Jul-1994 |
lcp <none@none> |
Axiom of choice, cardinality results, etc.
|
| #
f16078bc |
|
12-Jul-1994 |
lcp <none@none> |
new cardinal arithmetic developments
|
| #
ba6b9f3c |
|
21-Jun-1994 |
lcp <none@none> |
Addition of cardinals and order types, various tidying
|
| #
fae5ec30 |
|
16-Mar-1994 |
lcp <none@none> |
Improved layout for inductive defs
|
| #
e2ba328e |
|
30-Sep-1993 |
lcp <none@none> |
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
domrange/image_subset,vimage_subset: deleted needless premise!
misc: This slightly simplifies two proofs in Schroeder-Bernstein Theorem
ind-syntax/rule_concl: recoded to avoid exceptions
intr-elim: now checks conclusions of introduction rules
func/fun_disjoint_Un: now uses ex_ex1I
list-fn/hd,tl,drop: new
simpdata/bquant_simps: new
list/list_case_type: restored!
bool.thy: changed 1 from a "def" to a translation
Removed occurreces of one_def in bool.ML, nat.ML, univ.ML, ex/integ.ML
nat/succ_less_induct: new induction principle
arith/add_mono: new results about monotonicity
simpdata/mem_simps: removed the ones for succ and cons; added succI1,
consI2 to ZF_ss
upair/succ_iff: new, for use with simp_tac (cons_iff already existed)
ordinal/Ord_0_in_succ: renamed from Ord_0_mem_succ
nat/nat_0_in_succ: new
ex/prop-log/hyps_thms_if: split up the fast_tac call for more speed
|
| #
ce0256d3 |
|
17-Sep-1993 |
lcp <none@none> |
Installation of new simplifier for ZF. Deleted all congruence rules not
involving local assumptions. NB the congruence rules for Sigma and Pi
(dependent type constructions) cause difficulties and are not used by
default.
|
| #
f253ef6a |
|
15-Sep-1993 |
clasohm <none@none> |
Initial revision
|