| Thu, 14 Dec 2006 21:33:47 +0100 | huffman | prove hyperpow_realpow using transfer | changeset | files |
| Thu, 14 Dec 2006 21:03:39 +0100 | huffman | remove usage of ultra tactic | changeset | files |
| Thu, 14 Dec 2006 19:29:48 +0100 | huffman | add lemmas singleton and insert_iff | changeset | files |
| Thu, 14 Dec 2006 19:15:16 +0100 | huffman | generalized type of hyperpow; removed hcpow | changeset | files |
| Thu, 14 Dec 2006 18:10:38 +0100 | huffman | redefine hSuc as *f* Suc, and move to HyperNat.thy | changeset | files |
| Thu, 14 Dec 2006 16:08:09 +0100 | wenzelm | proper use of IntInf instead of InfInf; | changeset | files |
| Thu, 14 Dec 2006 15:31:22 +0100 | wenzelm | defs/notes: more robust transitivity reasoning; | changeset | files |