2000-09-07 |
wenzelm |
tuned ML code (the_context, bind_thms(s));
|
file |
diff |
annotate
|
2000-09-05 |
paulson |
new AddIffs (especially Memrel_iff)
|
file |
diff |
annotate
|
2000-08-01 |
paulson |
natify, a coercion to reduce the number of type constraints in arithmetic
|
file |
diff |
annotate
|
2000-06-28 |
paulson |
tidying and unbatchifying
|
file |
diff |
annotate
|
2000-03-22 |
paulson |
tidied using new "inst" rule
|
file |
diff |
annotate
|
2000-02-07 |
paulson |
tidied some proofs
|
file |
diff |
annotate
|
2000-01-13 |
paulson |
new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
|
file |
diff |
annotate
|
1999-09-07 |
wenzelm |
isatool expandshort;
|
file |
diff |
annotate
|
1999-02-03 |
paulson |
tidied, with left_inverse & right_inverse as default simprules
|
file |
diff |
annotate
|
1999-01-27 |
paulson |
new typechecking solver for the simplifier
|
file |
diff |
annotate
|
1999-01-07 |
paulson |
ZF: the natural numbers as a datatype
|
file |
diff |
annotate
|
1999-01-07 |
paulson |
if-then-else syntax for ZF
|
file |
diff |
annotate
|
1998-09-22 |
paulson |
tidying
|
file |
diff |
annotate
|
1998-09-15 |
paulson |
tidied
|
file |
diff |
annotate
|
1998-08-17 |
paulson |
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
|
file |
diff |
annotate
|
1998-08-10 |
paulson |
Tidying of AC, especially of AC16_WO4 using a locale
|
file |
diff |
annotate
|
1998-07-15 |
paulson |
More tidying and removal of "\!\!... from Goal commands
|
file |
diff |
annotate
|
1998-07-13 |
paulson |
Huge tidy-up: removal of leading \!\!
|
file |
diff |
annotate
|
1998-07-02 |
paulson |
Renamed expand_if to split_if and setloop split_tac to addsplits,
|
file |
diff |
annotate
|
1998-06-22 |
wenzelm |
isatool fixgoal;
|
file |
diff |
annotate
|
1997-12-24 |
paulson |
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
|
file |
diff |
annotate
|
1997-11-27 |
paulson |
Tidying, mostly indentation
|
file |
diff |
annotate
|
1997-11-05 |
paulson |
Ran expandshort, especially to introduce Safe_tac
|
file |
diff |
annotate
|
1997-11-03 |
wenzelm |
isatool fixclasimp;
|
file |
diff |
annotate
|
1997-10-16 |
wenzelm |
transfer CardinalArith.thy nat_into_Ord;
|
file |
diff |
annotate
|
1997-10-10 |
wenzelm |
fixed dots;
|
file |
diff |
annotate
|
1997-09-29 |
paulson |
Much tidying including step_tac -> clarify_tac or safe_tac; sometimes
|
file |
diff |
annotate
|
1997-04-23 |
paulson |
Conversion to use blast_tac
|
file |
diff |
annotate
|
1997-04-09 |
paulson |
Using Blast_tac
|
file |
diff |
annotate
|
1997-01-08 |
paulson |
Removal of sum_cs and eq_cs
|
file |
diff |
annotate
|
1997-01-03 |
paulson |
Implicit simpsets and clasets for FOL and ZF
|
file |
diff |
annotate
|
1996-03-28 |
paulson |
New theorem Finite_imp_succ_cardinal_Diff
|
file |
diff |
annotate
|
1996-03-26 |
paulson |
New lemmas for Mutilated Checkerboard
|
file |
diff |
annotate
|
1996-01-30 |
clasohm |
expanded tabs
|
file |
diff |
annotate
|
1995-05-03 |
lcp |
Changed some definitions and proofs to use pattern-matching.
|
file |
diff |
annotate
|
1995-04-28 |
lcp |
Modified proofs for new claset primitives. The problem is that they enforce
|
file |
diff |
annotate
|
1995-03-31 |
lcp |
Tried the new addss in a proof.
|
file |
diff |
annotate
|
1995-01-20 |
lcp |
Replaced ordermap_z_lepoll by ordermap_z_lt, which is
|
file |
diff |
annotate
|
1995-01-11 |
lcp |
Now proof of Ord_jump_cardinal uses
|
file |
diff |
annotate
|
1994-12-23 |
lcp |
Changed succ(1) to 2 in cmult_2; Simplified proof of InfCard_is_Limit
|
file |
diff |
annotate
|
1994-12-16 |
lcp |
Limit_csucc: moved to InfDatatype and proved explicitly in
|
file |
diff |
annotate
|
1994-12-14 |
clasohm |
added bind_thm for theorems defined by "standard ..."
|
file |
diff |
annotate
|
1994-12-08 |
lcp |
sum_lepoll_self, cadd_le_self, prod_lepoll_self,
|
file |
diff |
annotate
|
1994-12-07 |
clasohm |
added qed and qed_goal[w]
|
file |
diff |
annotate
|
1994-08-22 |
lcp |
ZF/Cardinal: some results moved here from CardinalArith
|
file |
diff |
annotate
|
1994-08-15 |
lcp |
ZF/CardinalArith/InfCard_Un: new
|
file |
diff |
annotate
|
1994-08-12 |
lcp |
for infinite datatypes with arbitrary index sets
|
file |
diff |
annotate
|
1994-08-12 |
lcp |
installation of new inductive/datatype sections
|
file |
diff |
annotate
|
1994-07-27 |
lcp |
Addition of infinite branching datatypes
|
file |
diff |
annotate
|
1994-07-26 |
lcp |
Axiom of choice, cardinality results, etc.
|
file |
diff |
annotate
|
1994-07-12 |
lcp |
new cardinal arithmetic developments
|
file |
diff |
annotate
|
1994-06-23 |
lcp |
modifications for cardinal arithmetic
|
file |
diff |
annotate
|