1999-01-27 |
paulson |
new typechecking solver for the simplifier
|
file |
diff |
annotate
|
1999-01-19 |
paulson |
removal of the (thm list) argument of mk_cases
|
file |
diff |
annotate
|
1999-01-13 |
paulson |
datatype package improvements
|
file |
diff |
annotate
|
1999-01-07 |
paulson |
ZF: the natural numbers as a datatype
|
file |
diff |
annotate
|
1999-01-06 |
paulson |
induct_tac and exhaust_tac
|
file |
diff |
annotate
|
1998-12-28 |
paulson |
new inductive, datatype and primrec packages, etc.
|
file |
diff |
annotate
|
1998-09-22 |
paulson |
tidying
|
file |
diff |
annotate
|
1998-08-14 |
paulson |
got rid of some goal thy commands
|
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-06-22 |
wenzelm |
isatool fixgoal;
|
file |
diff |
annotate
|
1997-11-03 |
wenzelm |
isatool fixclasimp;
|
file |
diff |
annotate
|
1997-10-10 |
wenzelm |
fixed dots;
|
file |
diff |
annotate
|
1997-04-23 |
paulson |
Conversion to use blast_tac
|
file |
diff |
annotate
|
1997-02-15 |
oheimb |
reflecting my recent changes of the simplifier and classical reasoner
|
file |
diff |
annotate
|
1997-01-09 |
paulson |
Removal of needless "addIs [equality]", etc.
|
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-08-20 |
paulson |
Addition of function set_of_list
|
file |
diff |
annotate
|
1996-04-18 |
oheimb |
adapted proof of drop_succ_Cons: problem with non-confluent simpset removed
|
file |
diff |
annotate
|
1996-01-30 |
clasohm |
expanded tabs
|
file |
diff |
annotate
|
1995-02-27 |
lcp |
Updated comment about list_subset_univ and list_into_univ.
|
file |
diff |
annotate
|
1994-12-14 |
clasohm |
added bind_thm for theorems defined by "standard ..."
|
file |
diff |
annotate
|
1994-12-07 |
clasohm |
added qed and qed_goal[w]
|
file |
diff |
annotate
|
1994-08-15 |
lcp |
ZF/List, ex/Brouwer,Data,LList,Ntree,TF,Term: much simplified proof of _unfold
|
file |
diff |
annotate
|
1994-08-12 |
lcp |
installation of new inductive/datatype sections
|
file |
diff |
annotate
|
1994-07-26 |
lcp |
Axiom of choice, cardinality results, etc.
|
file |
diff |
annotate
|
1994-07-15 |
clasohm |
added thy_name to Datatype_Fun's parameter
|
file |
diff |
annotate
|
1994-07-01 |
clasohm |
replaced extend_theory by new add_* functions;
|
file |
diff |
annotate
|