| Fri, 21 Oct 2005 18:14:50 +0200 |
wenzelm |
Goal.conclude;
|
file |
diff |
annotate
|
| Thu, 02 Jun 2005 09:11:32 +0200 |
wenzelm |
header;
|
file |
diff |
annotate
|
| Fri, 13 May 2005 20:21:41 +0200 |
dixon |
lucas - fixed bug with uninstantiated type contexts in eqsubst and added the automatic removal of duplicate subgoals (when there are no flex-flex constraints)
|
file |
diff |
annotate
|
| Thu, 05 May 2005 11:58:59 +0200 |
dixon |
lucas - made clean unify smash unifiers so that when we get flex-flex constraints subst does not barf. Also added fix_vars_upto_idx to IsaND.
|
file |
diff |
annotate
|
| Wed, 04 May 2005 10:44:53 +0200 |
paulson |
eta-expansion
|
file |
diff |
annotate
|
| Tue, 03 May 2005 02:45:55 +0200 |
dixon |
lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.
|
file |
diff |
annotate
|
| Tue, 26 Apr 2005 20:38:15 +0200 |
dixon |
lucas - improved comments, clarified function behaviour, added missing functions for working with meta variables.
|
file |
diff |
annotate
|
| Fri, 04 Mar 2005 15:07:34 +0100 |
skalberg |
Removed practically all references to Library.foldr.
|
file |
diff |
annotate
|
| Thu, 03 Mar 2005 12:43:01 +0100 |
skalberg |
Move towards standard functions.
|
file |
diff |
annotate
|
| Sun, 13 Feb 2005 17:15:14 +0100 |
skalberg |
Deleted Library.option type.
|
file |
diff |
annotate
|
| Tue, 01 Feb 2005 18:01:57 +0100 |
paulson |
the new subst tactic, by Lucas Dixon
|
file |
diff |
annotate
|