Mon, 28 Feb 2000 10:49:08 +0100 | paulson | new thm vimage_Collect_eq | changeset | files |
Mon, 28 Feb 2000 10:48:39 +0100 | paulson | more bijection theorems | changeset | files |
Sun, 27 Feb 2000 15:33:35 +0100 | wenzelm | cases/induct attributes; | changeset | files |
Sun, 27 Feb 2000 15:32:10 +0100 | wenzelm | add_cases_induct: induct_method setup; | changeset | files |
Sun, 27 Feb 2000 15:31:40 +0100 | wenzelm | HOLogic.dest_conj; | changeset | files |
Sun, 27 Feb 2000 15:26:47 +0100 | wenzelm | HOLogic.dest_conj; | changeset | files |
Sun, 27 Feb 2000 15:25:31 +0100 | wenzelm | even better induct setup; | changeset | files |