| Wed, 18 Mar 2015 15:23:12 +0100 | noschinl | merged | changeset | files |
| Wed, 18 Mar 2015 13:51:33 +0100 | noschinl | added proof method rewrite | changeset | files |
| Wed, 18 Mar 2015 13:31:52 +0100 | wenzelm | merged | changeset | files |
| Tue, 17 Mar 2015 16:38:09 +0100 | wenzelm | tuned; | changeset | files |
| 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 |
| Tue, 17 Mar 2015 09:22:21 +0100 | nipkow | merged | changeset | files |
| Tue, 17 Mar 2015 09:22:17 +0100 | nipkow | added lemmas | changeset | files |
| Mon, 16 Mar 2015 23:05:56 +0100 | traytel | document property | changeset | files |
| Mon, 16 Mar 2015 23:05:56 +0100 | traytel | BNF relators preserve reflexivity | changeset | files |
| Mon, 16 Mar 2015 23:00:38 +0100 | blanchet | export more ML functions | changeset | files |
| Mon, 16 Mar 2015 17:47:46 +0100 | wenzelm | merged | changeset | files |
| Mon, 16 Mar 2015 17:26:46 +0100 | wenzelm | suppress semantic completion in errors of batch build -- avoid junk in log files; | changeset | files |
| Mon, 16 Mar 2015 17:02:00 +0100 | blanchet | updated docs | changeset | files |
| Mon, 16 Mar 2015 17:01:59 +0100 | blanchet | clarified documentation | changeset | files |
| Mon, 16 Mar 2015 16:59:59 +0100 | wenzelm | proper headers; | changeset | files |
| Mon, 16 Mar 2015 16:26:33 +0100 | wenzelm | merged | changeset | files |
| Mon, 16 Mar 2015 16:26:02 +0100 | wenzelm | tuned message -- include completion; | changeset | files |
| Mon, 16 Mar 2015 15:33:32 +0100 | wenzelm | support for completion reports produced in Scala (inlined into messages); | changeset | files |
| Mon, 16 Mar 2015 14:15:15 +0100 | wenzelm | more precises positions; | changeset | files |
| Mon, 16 Mar 2015 13:32:31 +0100 | wenzelm | avoid duplicate header errors, more precise positions; | changeset | files |
| Mon, 16 Mar 2015 11:30:54 +0100 | wenzelm | tuned protocol -- resolve command positions in ML; | changeset | files |
| Mon, 16 Mar 2015 11:07:56 +0100 | wenzelm | clarified modules; | changeset | files |
| Mon, 16 Mar 2015 14:52:34 +0100 | hoelzl | add inequalities (move from AFP/Amortized_Complexity) | changeset | files |
| Sun, 15 Mar 2015 23:46:00 +0100 | blanchet | merge | changeset | files |