| 1998-03-09 |
wenzelm |
1998-03-09 |
adapted to baroque chars;
|
file | diff | annotate |
| 1998-03-04 |
nipkow |
1998-03-04 |
Reorganized simplifier. May now reorient rules.
Moved loop tests from logic to thm.
|
file | diff | annotate |
| 1998-02-28 |
nipkow |
1998-02-28 |
Tried to reorganize rewriter a little. More to be done.
|
file | diff | annotate |
| 1998-02-18 |
nipkow |
1998-02-18 |
Improved loop-test for rewrite rules a little.
Should be done properly!
|
file | diff | annotate |
| 1997-12-19 |
wenzelm |
1997-12-19 |
term order stuff moved to term.ML;
|
file | diff | annotate |
| 1997-12-02 |
wenzelm |
1997-12-02 |
tuned term order;
added indexname_ord, typ_ord, typs_ord, term_ord, terms_ord;
|
file | diff | annotate |
| 1997-11-28 |
nipkow |
1997-11-28 |
Fixed the definition of `termord': is now antisymmetric.
|
file | diff | annotate |
| 1997-11-04 |
nipkow |
1997-11-04 |
logic: loops -> rewrite_rule_ok
added rewrite_rule_extra_vars
thm: Rewrite rules must not introduce new type vars on rhs.
This lead to an incompleteness, is now banned, and the code
has been simplified.
|
file | diff | annotate |
| 1997-10-21 |
nipkow |
1997-10-21 |
Corrected alphabetical order of entries in signature.
|
file | diff | annotate |
| 1997-10-17 |
paulson |
1997-10-17 |
Added "op" before "occs" to make sml/nj happy
|
file | diff | annotate |
| 1997-10-16 |
nipkow |
1997-10-16 |
The simplifier has been improved a little: equations s=t which used to be
rejected because of looping are now treated as (s=t) == True. The latter
translation must be done outside of Thm because it involves the object-logic
specific True. Therefore the simple loop test has been moved from Thm to
Logic.
|
file | diff | annotate |
| 1997-06-05 |
paulson |
1997-06-05 |
Removal of freeze_vars and thaw_vars (quite unused...)
|
file | diff | annotate |
| 1997-01-16 |
wenzelm |
1997-01-16 |
added term order;
|
file | diff | annotate |
| 1996-11-28 |
paulson |
1996-11-28 |
Replaced map...~~ by ListPair.map
|
file | diff | annotate |
| 1996-06-28 |
paulson |
1996-06-28 |
Restored warning comment
|
file | diff | annotate |
| 1996-02-16 |
paulson |
1996-02-16 |
Elimination of fully-functorial style.
Type tactic changed to a type abbrevation (from a datatype).
Constructor tactic and function apply deleted.
|
file | diff | annotate |
| 1996-01-29 |
clasohm |
1996-01-29 |
inserted tabs again
|
file | diff | annotate |
| 1996-01-29 |
clasohm |
1996-01-29 |
removed tabs
|
file | diff | annotate |
| 1994-10-12 |
wenzelm |
1994-10-12 |
added is_equals: term -> bool;
|
file | diff | annotate |
| 1994-09-06 |
lcp |
1994-09-06 |
Pure/type/unvarifyT: moved there from logic.ML
|
file | diff | annotate |
| 1994-08-18 |
lcp |
1994-08-18 |
/unvarifyT, unvarify: moved to Pure/logic.ML
|
file | diff | annotate |
| 1994-07-06 |
wenzelm |
1994-07-06 |
changed comment only;
|
file | diff | annotate |
| 1994-05-26 |
wenzelm |
1994-05-26 |
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
restored functor sig constraint :LOGIC;
|
file | diff | annotate |
| 1994-01-04 |
wenzelm |
1994-01-04 |
commented out sig constraint of functor (for debugging purposes);
|
file | diff | annotate |
| 1993-10-21 |
lcp |
1993-10-21 |
logic/mk_equals,mk_flexpair: now calls fastype_of instead of type_of.
So it no longer checks t properly -- but it never checked u anyway, and all
existing calls are derived from certified terms...
|
file | diff | annotate |
| 1993-09-16 |
clasohm |
1993-09-16 |
Initial revision
|
file | diff | annotate |