[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Isarmathlib-devel] Direct product
|
From: |
Sanghyeon Seo |
|
Subject: |
[Isarmathlib-devel] Direct product |
|
Date: |
Thu, 5 Jun 2008 04:06:23 +0900 |
Hi, this is my first post.
Attached is my attempt at definition of direct product and proof of
some properties. This is my first Isabelle theory, so any suggestion
is welcome. It took incredibly long time to get this done, but I think
I now understand how things are done.
--
Seo Sanghyeon
DirectProduct_ZF.thy
Description: Binary data
- [Isarmathlib-devel] Direct product,
Sanghyeon Seo <=