| Wed, 28 Jan 2009 16:57:12 +0100 |
nipkow |
merged - resolving conflics
|
file |
diff |
annotate
|
| Wed, 28 Jan 2009 16:29:16 +0100 |
nipkow |
Replaced group_ and ring_simps by algebra_simps;
|
file |
diff |
annotate
|
| Wed, 28 Jan 2009 11:04:10 +0100 |
haftmann |
Reflection.thy now in HOL/Library
|
file |
diff |
annotate
|
| Thu, 20 Nov 2008 19:43:34 +0100 |
wenzelm |
reactivated some dead theories (based on hints by Mark Hillebrand);
|
file |
diff |
annotate
|
| Sun, 08 Jul 2007 19:01:32 +0200 |
chaieb |
Show the use of reflection attribute; fixed comments about the order of absorbing equations : f (C x) = x ; now automaically tried as last;
|
file |
diff |
annotate
|
| Sat, 07 Jul 2007 11:09:40 +0200 |
chaieb |
The order for parameter for interpretation is now inversted:
|
file |
diff |
annotate
|
| Fri, 06 Jul 2007 16:09:28 +0200 |
chaieb |
Some examples for reifying type variables
|
file |
diff |
annotate
|
| Tue, 03 Jul 2007 17:49:58 +0200 |
chaieb |
More examples
|
file |
diff |
annotate
|
| Sat, 23 Jun 2007 19:33:22 +0200 |
nipkow |
tuned and renamed group_eq_simps and ring_eq_simps
|
file |
diff |
annotate
|
| Sun, 28 Jan 2007 11:52:52 +0100 |
chaieb |
Now deals with simples cases where the input equations contain type variables
|
file |
diff |
annotate
|
| Mon, 18 Sep 2006 10:09:57 +0200 |
chaieb |
Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n)
|
file |
diff |
annotate
|
| Mon, 11 Sep 2006 21:35:19 +0200 |
wenzelm |
induct method: renamed 'fixing' to 'arbitrary';
|
file |
diff |
annotate
|
| Mon, 14 Aug 2006 11:13:50 +0200 |
chaieb |
Reification now handels binders.
|
file |
diff |
annotate
|
| Fri, 04 Aug 2006 12:01:31 +0200 |
chaieb |
*** empty log message ***
|
file |
diff |
annotate
|
| Thu, 03 Aug 2006 15:03:05 +0200 |
wenzelm |
Generic reflection and reification (by Amine Chaieb).
|
file |
diff |
annotate
|