| Wed, 18 Aug 2004 11:09:40 +0200 |
nipkow |
import -> imports
|
file |
diff |
annotate
|
| Mon, 16 Aug 2004 14:22:27 +0200 |
nipkow |
New theory header syntax.
|
file |
diff |
annotate
|
| Wed, 04 Aug 2004 19:09:41 +0200 |
nipkow |
added a few thms
|
file |
diff |
annotate
|
| Fri, 23 Apr 2004 11:04:07 +0200 |
paulson |
congruent2 now allows different equiv relations
|
file |
diff |
annotate
|
| Fri, 02 Apr 2004 17:06:15 +0200 |
paulson |
variable renamings and other cosmetic changes
|
file |
diff |
annotate
|
| Tue, 30 Mar 2004 11:18:12 +0200 |
paulson |
tidied
|
file |
diff |
annotate
|
| Tue, 27 Jan 2004 15:39:51 +0100 |
paulson |
replacing HOL/Real/PRat, PNat by the rational number development
|
file |
diff |
annotate
|
| Tue, 18 Nov 2003 11:01:52 +0100 |
paulson |
conversion of ML to Isar scripts
|
file |
diff |
annotate
|
| Thu, 08 Aug 2002 23:47:41 +0200 |
wenzelm |
converted;
|
file |
diff |
annotate
|
| Thu, 06 Dec 2001 00:40:04 +0100 |
wenzelm |
renamed Finite to Finite_Set;
|
file |
diff |
annotate
|
| Tue, 09 Jan 2001 15:32:27 +0100 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Fri, 05 Jan 2001 18:48:18 +0100 |
nipkow |
^^ -> ```
|
file |
diff |
annotate
|
| Wed, 19 Jul 2000 12:33:36 +0200 |
paulson |
changed / to // for quotienting
|
file |
diff |
annotate
|
| Thu, 10 Jun 1999 10:40:57 +0200 |
paulson |
moved predicates refl, sym down to Relation.thy
|
file |
diff |
annotate
|
| Fri, 30 May 1997 15:21:53 +0200 |
paulson |
Addition of Finite as parent allows cardinality theorems
|
file |
diff |
annotate
|
| Thu, 21 Nov 1996 15:28:25 +0100 |
paulson |
Tidied up some proofs, ...
|
file |
diff |
annotate
|
| Thu, 04 Apr 1996 11:45:01 +0200 |
paulson |
Using new "Times" infix
|
file |
diff |
annotate
|
| Mon, 05 Feb 1996 21:29:06 +0100 |
clasohm |
expanded tabs; incorporated Konrad's changes
|
file |
diff |
annotate
|
| Wed, 21 Jun 1995 15:47:10 +0200 |
clasohm |
removed \...\ inside strings
|
file |
diff |
annotate
|
| Fri, 24 Mar 1995 12:30:35 +0100 |
clasohm |
changed syntax of tuples from <..., ...> to (..., ...)
|
file |
diff |
annotate
|
| Fri, 03 Mar 1995 12:04:45 +0100 |
clasohm |
new version of HOL/Integ with curried function application
|
file |
diff |
annotate
|