| Mon, 31 Jan 2000 16:18:42 +0100 | paulson | new theorem rev_ImageI | changeset | files |
| Mon, 31 Jan 2000 16:18:09 +0100 | paulson | various theorems about image and inverse image | changeset | files |
| Mon, 31 Jan 2000 16:13:28 +0100 | paulson | Pi_empty1 is a more general simprule than empty_fun | changeset | files |
| Sun, 30 Jan 2000 13:24:41 +0100 | wenzelm | rm -f *.aux; | changeset | files |
| Sat, 29 Jan 2000 14:22:16 +0100 | wenzelm | simp_all method; | changeset | files |
| Fri, 28 Jan 2000 21:58:39 +0100 | wenzelm | eliminated proof script; | changeset | files |
| Fri, 28 Jan 2000 21:57:15 +0100 | wenzelm | HEADGOAL; | changeset | files |
| Fri, 28 Jan 2000 21:56:55 +0100 | wenzelm | added prefer, defer; | changeset | files |
| Fri, 28 Jan 2000 21:56:37 +0100 | wenzelm | added HEADGOAL; | changeset | files |
| Fri, 28 Jan 2000 21:56:02 +0100 | wenzelm | added defer, prefer; | changeset | files |
| Fri, 28 Jan 2000 21:55:43 +0100 | wenzelm | Drule.instantiate; | changeset | files |
| Fri, 28 Jan 2000 21:55:23 +0100 | wenzelm | cp -r; | changeset | files |
| Fri, 28 Jan 2000 15:26:51 +0100 | wenzelm | -p option; | changeset | files |
| Fri, 28 Jan 2000 15:08:15 +0100 | oheimb | added range_composition (also to simpset) | changeset | files |
| Fri, 28 Jan 2000 14:49:00 +0100 | oheimb | added finite_range_updI, finite_range_map_of, finite_range_map_of_override | changeset | files |
| Fri, 28 Jan 2000 14:42:46 +0100 | wenzelm | mkdir: prepare logic session directory; | changeset | files |
| Fri, 28 Jan 2000 14:09:23 +0100 | oheimb | added full_nat_induct | changeset | files |
| Fri, 28 Jan 2000 14:08:54 +0100 | oheimb | added splitE', also to claset | changeset | files |
| Fri, 28 Jan 2000 14:07:53 +0100 | oheimb | added inj_singleton | changeset | files |
| Fri, 28 Jan 2000 14:07:33 +0100 | oheimb | added finite_range_imageI | changeset | files |
| Fri, 28 Jan 2000 12:12:06 +0100 | wenzelm | replaced FIRSTGOAL by FINDGOAL (backtracking!); | changeset | files |
| Fri, 28 Jan 2000 12:10:47 +0100 | wenzelm | maintain standard rules (beware: classical provers provides another version!); | changeset | files |
| Fri, 28 Jan 2000 12:06:52 +0100 | wenzelm | replaced FIRSTGOAL by FINDGOAL (backtracking!); | changeset | files |
| Fri, 28 Jan 2000 12:04:17 +0100 | wenzelm | tuned sig; | changeset | files |
| Fri, 28 Jan 2000 12:03:59 +0100 | wenzelm | map data; | changeset | files |
| Fri, 28 Jan 2000 11:23:41 +0100 | oheimb | added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED | changeset | files |
| Fri, 28 Jan 2000 11:22:02 +0100 | oheimb | beautified spacing for binders with symbols syntax, analogous to HOL.thy | changeset | files |
| Thu, 27 Jan 2000 15:30:10 +0100 | oheimb | *** empty log message *** | changeset | files |