| Thu, 05 Jan 2006 17:16:40 +0100 |
wenzelm |
proper handling of simultaneous goals and mutual rules;
|
file |
diff |
annotate
|
| Thu, 01 Dec 2005 04:46:17 +0100 |
urbanc |
changed "fresh:" to "avoiding:" and cleaned up the weakening example
|
file |
diff |
annotate
|
| Wed, 30 Nov 2005 15:24:32 +0100 |
wenzelm |
added rename_params_rule: recover orginal fresh names in subgoals/cases;
|
file |
diff |
annotate
|
| Wed, 30 Nov 2005 14:27:50 +0100 |
wenzelm |
fresh: frees instead of terms, rename corresponding params in rule;
|
file |
diff |
annotate
|
| Wed, 30 Nov 2005 00:46:08 +0100 |
wenzelm |
proper treatment of tuple/tuple_fun -- nest to the left!
|
file |
diff |
annotate
|
| Tue, 29 Nov 2005 18:09:12 +0100 |
wenzelm |
reworked version with proper support for defs, fixes, fresh specification;
|
file |
diff |
annotate
|
| Sun, 27 Nov 2005 05:09:43 +0100 |
urbanc |
some minor tunings
|
file |
diff |
annotate
|
| Sun, 13 Nov 2005 22:36:30 +0100 |
urbanc |
changed the HOL_basic_ss back and selectively added
|
file |
diff |
annotate
|
| Sun, 13 Nov 2005 20:33:36 +0100 |
urbanc |
exchanged HOL_ss for HOL_basic_ss in the simplification
|
file |
diff |
annotate
|
| Mon, 07 Nov 2005 10:47:25 +0100 |
urbanc |
fixed bug with nominal induct
|
file |
diff |
annotate
|
| Tue, 01 Nov 2005 23:54:29 +0100 |
urbanc |
tunings of some comments (nothing serious)
|
file |
diff |
annotate
|
| Mon, 17 Oct 2005 12:30:57 +0200 |
berghofe |
Initial revision.
|
file |
diff |
annotate
|