| 1997-10-17 |
nipkow |
Removed image_eqI from simpset because of clash with neq_shrK.
|
changeset |
files
|
| 1997-10-16 |
nipkow |
AddIffs [all_not_in_conv];
|
changeset |
files
|
| 1997-10-16 |
wenzelm |
global;
|
changeset |
files
|
| 1997-10-16 |
nipkow |
Modified comment.
|
changeset |
files
|
| 1997-10-16 |
paulson |
New simprules imp_disj1, imp_disj2
|
changeset |
files
|
| 1997-10-16 |
paulson |
New simprule diff_le_self, requiring a new proof of diff_diff_cancel
|
changeset |
files
|
| 1997-10-16 |
nipkow |
Removed comment.
|
changeset |
files
|
| 1997-10-16 |
wenzelm |
tuned;
|
changeset |
files
|
| 1997-10-16 |
wenzelm |
removed begin;
|
changeset |
files
|
| 1997-10-16 |
wenzelm |
fixed prep_ext;
|
changeset |
files
|
| 1997-10-16 |
nipkow |
Simplified proof.
|
changeset |
files
|
| 1997-10-16 |
nipkow |
Simplified proof because of better simplifier.
|
changeset |
files
|
| 1997-10-16 |
nipkow |
Various new lemmas. Improved conversion of equations to rewrite rules:
|
changeset |
files
|
| 1997-10-16 |
wenzelm |
added transfer: theory -> thm -> thm;
|
changeset |
files
|
| 1997-10-16 |
wenzelm |
oops;
|
changeset |
files
|
| 1997-10-16 |
nipkow |
The simplifier has been improved a little: equations s=t which used to be
|
changeset |
files
|
| 1997-10-16 |
wenzelm |
fixed dependencies;
|
changeset |
files
|
| 1997-10-16 |
wenzelm |
transfer thy Ord_nat;
|
changeset |
files
|
| 1997-10-16 |
wenzelm |
sevaral goals restated in mono.thy;
|
changeset |
files
|
| 1997-10-16 |
wenzelm |
moved rank_Inl, rank_Inr from Epsilon.ML to Univ.ML;
|
changeset |
files
|
| 1997-10-16 |
wenzelm |
transfer InfDatatype.thy Limit_VfromE;
|
changeset |
files
|
| 1997-10-16 |
wenzelm |
transfer CardinalArith.thy nat_into_Ord;
|
changeset |
files
|
| 1997-10-16 |
wenzelm |
improved pretty_arity;
|
changeset |
files
|
| 1997-10-16 |
wenzelm |
added merge_theories (new name arg);
|
changeset |
files
|
| 1997-10-16 |
wenzelm |
fixed merge_theories;
|
changeset |
files
|
| 1997-10-16 |
wenzelm |
revert to 1.3;
|
changeset |
files
|
| 1997-10-16 |
wenzelm |
revert to 1.1;
|
changeset |
files
|
| 1997-10-16 |
nipkow |
Added last, butlast, dropped ttl.
|
changeset |
files
|
| 1997-10-16 |
mueller |
lala
|
changeset |
files
|
| 1997-10-16 |
paulson |
Eta-expansion of function declarations, for value polymorphism
|
changeset |
files
|
| 1997-10-15 |
wenzelm |
remove merge_theories;
|
changeset |
files
|
| 1997-10-15 |
wenzelm |
make_draft replaced by prep_ext;
|
changeset |
files
|
| 1997-10-15 |
wenzelm |
tuned;
|
changeset |
files
|
| 1997-10-15 |
wenzelm |
eliminated aliasing merge: now always extends;
|
changeset |
files
|
| 1997-10-15 |
wenzelm |
tuned comment;
|
changeset |
files
|
| 1997-10-15 |
wenzelm |
improved print_data;
|
changeset |
files
|
| 1997-10-15 |
wenzelm |
tuned;
|
changeset |
files
|
| 1997-10-15 |
wenzelm |
slightly changed interfaces for oracles;
|
changeset |
files
|
| 1997-10-15 |
nipkow |
Added ack to Mateja Jamnik.
|
changeset |
files
|
| 1997-10-15 |
wenzelm |
tuned;
|
changeset |
files
|
| 1997-10-14 |
wenzelm |
tuned;
|
changeset |
files
|
| 1997-10-14 |
wenzelm |
added additional generic data;
|
changeset |
files
|
| 1997-10-14 |
wenzelm |
Sign.print_data;
|
changeset |
files
|
| 1997-10-14 |
wenzelm |
added init_data, get_data, put_data;
|
changeset |
files
|
| 1997-10-14 |
wenzelm |
added data.ML;
|
changeset |
files
|
| 1997-10-14 |
wenzelm |
Arbitrarily typed data.
|
changeset |
files
|
| 1997-10-14 |
paulson |
Patch to avoid simplification of ~EX to ALL~
|
changeset |
files
|
| 1997-10-14 |
nipkow |
Two lemmas are already in List.
|
changeset |
files
|
| 1997-10-14 |
nipkow |
More lemmas, esp. ~Bex and ~Ball conversions.
|
changeset |
files
|
| 1997-10-14 |
nipkow |
Added neagtion rules for Ball and Bex.
|
changeset |
files
|
| 1997-10-14 |
wenzelm |
tuned;
|
changeset |
files
|
| 1997-10-14 |
wenzelm |
browser info;
|
changeset |
files
|
| 1997-10-14 |
paulson |
rearranged and added TLA
|
changeset |
files
|
| 1997-10-13 |
wenzelm |
fixed extern;
|
changeset |
files
|
| 1997-10-13 |
wenzelm |
uses Sign.str_of_classrel, Sign.str_of_arity, Sign.str_of_arity;
|
changeset |
files
|
| 1997-10-13 |
wenzelm |
uses Sign.str_of_sort;
|
changeset |
files
|
| 1997-10-13 |
wenzelm |
fixed dots;
|
changeset |
files
|
| 1997-10-13 |
wenzelm |
print_goals: optional output of const types (set show_consts);
|
changeset |
files
|
| 1997-10-13 |
wenzelm |
merge: drops path elements;
|
changeset |
files
|
| 1997-10-13 |
merz |
Absolute URL's for documentation
|
changeset |
files
|