| Tue, 17 Mar 2015 16:17:49 +0100 | wenzelm | tight span for theory header, which is relevant for error positions (including semantic completion); | changeset | files |
| Tue, 17 Mar 2015 15:21:41 +0100 | wenzelm | misc tuning and simplification; | changeset | files |
| Tue, 17 Mar 2015 17:45:03 +0000 | paulson | Inserted real_of_nat to fix factorial-related problem | changeset | files |
| Tue, 17 Mar 2015 15:11:25 +0000 | paulson | more general type class for factorial. Now allows code generation (?) | changeset | files |
| Tue, 17 Mar 2015 14:16:16 +0000 | paulson | Merge | changeset | files |
| Tue, 17 Mar 2015 12:23:56 +0000 | paulson | Merge | changeset | files |
| Mon, 16 Mar 2015 15:30:00 +0000 | paulson | The factorial function, "fact", now has type "nat => 'a" | changeset | files |