2000-10-13 |
paulson |
renamed fp_Tarski to fp_unfold
|
file |
diff |
annotate
|
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-24 |
paulson |
added some xsymbols, and tidied
|
file |
diff |
annotate
|
2000-06-30 |
paulson |
removal of batch-style proofs
|
file |
diff |
annotate
|
2000-06-28 |
paulson |
fixed some weak elim rules
|
file |
diff |
annotate
|
2000-06-21 |
paulson |
new theorems lepoll_Ord_imp_eqpoll, lesspoll_imp_eqpoll, lesspoll_nat_is_Finite
|
file |
diff |
annotate
|
2000-02-02 |
paulson |
expandshort
|
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-13 |
paulson |
datatype package improvements
|
file |
diff |
annotate
|
1999-01-07 |
paulson |
if-then-else syntax for ZF
|
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-08-06 |
paulson |
even more tidying of Goal commands
|
file |
diff |
annotate
|
1998-08-06 |
paulson |
Disjointness reasoning by AddEs [equals0E, sym RS equals0E]
|
file |
diff |
annotate
|
1998-08-04 |
paulson |
Renamed equals0D to equals0E
|
file |
diff |
annotate
|
1998-07-15 |
paulson |
More tidying and removal of "\!\!... from Goal commands
|
file |
diff |
annotate
|
1998-07-15 |
paulson |
Removal of leading "\!\!..." from most 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-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 |
oops;
|
file |
diff |
annotate
|
1997-10-16 |
wenzelm |
transfer thy Ord_nat;
|
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-04 |
paulson |
Another blast_tac call
|
file |
diff |
annotate
|
1997-04-02 |
paulson |
Mostly converted to blast_tac
|
file |
diff |
annotate
|
1997-03-18 |
paulson |
Stopped giving Introduction rules as Elimination rules
|
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-09-26 |
paulson |
Ran expandshort; used stac instead of ssubst
|
file |
diff |
annotate
|
1996-06-07 |
paulson |
Addition of converse_iff, domain_converse, range_converse as rewrites
|
file |
diff |
annotate
|
1996-05-01 |
paulson |
New lemma inspired by KG
|
file |
diff |
annotate
|
1996-03-28 |
paulson |
Ran expandshort
|
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-04-14 |
lcp |
Renamed diff_sing_lepoll, lepoll_diff_sing and diff_sing_eqpoll
|
file |
diff |
annotate
|
1995-04-13 |
lcp |
Proved lesspoll_succ_iff.
|
file |
diff |
annotate
|
1995-01-11 |
lcp |
Added Krzysztof's theorem LeastI2. Proof of sum_eqpoll_cong
|
file |
diff |
annotate
|
1994-12-23 |
lcp |
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
|
file |
diff |
annotate
|
1994-12-16 |
lcp |
changed useless "qed" calls for lemmas back to uses of "result",
|
file |
diff |
annotate
|
1994-12-15 |
lcp |
case_ss: now built upon ZF/Order/bij_inverse_ss. Deleted
|
file |
diff |
annotate
|
1994-12-14 |
clasohm |
added bind_thm for theorems defined by "standard ..."
|
file |
diff |
annotate
|
1994-12-08 |
lcp |
Card_cardinal_le: new
|
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/Cardinal/Card_Un: new
|
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
|
1994-06-21 |
lcp |
Addition of cardinals and order types, various tidying
|
file |
diff |
annotate
|