Sun, 25 Oct 2009 00:14:40 +0200 | Christian Urban | added data-storage about the quotients | changeset | files |
Sat, 24 Oct 2009 22:52:23 +0200 | Christian Urban | added another example file about integers (see HOL/Int.thy) | changeset | files |
Sat, 24 Oct 2009 18:17:38 +0200 | Christian Urban | changed the definitions of liftet constants to use fun_maps | changeset | files |
Sat, 24 Oct 2009 17:29:20 +0200 | cek | Merge | changeset | files |
Sat, 24 Oct 2009 17:29:27 +0200 | Cezary Kaliszyk | Finally lifted induction, with some manually added simplification lemmas. | changeset | files |
Sat, 24 Oct 2009 16:31:07 +0200 | Christian Urban | changed encoding from utf8 to ISO8 (needed to work with xemacs) | changeset | files |