| Mon, 23 Mar 2015 15:55:41 +0100 | wenzelm | tuned syntax diagrams -- no duplication of "target"; | changeset | files |
| Mon, 23 Mar 2015 15:54:41 +0100 | wenzelm | tuned; | changeset | files |
| Mon, 23 Mar 2015 14:56:52 +0100 | wenzelm | tuned; | changeset | files |
| Mon, 23 Mar 2015 13:30:59 +0100 | wenzelm | support 'for' fixes in rule_tac etc.; | changeset | files |
| Mon, 23 Mar 2015 15:08:02 +0100 | hoelzl | fix parameter order of NO_MATCH | changeset | files |
| Mon, 23 Mar 2015 10:16:20 +0100 | hoelzl | add measurable_submarkov | changeset | files |
| Mon, 23 Mar 2015 08:45:54 +0100 | nipkow | BT subsumed by Library/Tree | changeset | files |
| Mon, 23 Mar 2015 07:36:27 +0100 | nipkow | added funs and lemmas | changeset | files |
| Sun, 22 Mar 2015 13:10:34 +0100 | wenzelm | tuned; | changeset | files |
| Sun, 22 Mar 2015 12:45:34 +0100 | wenzelm | tuned; | changeset | files |
| Sun, 22 Mar 2015 12:38:41 +0100 | wenzelm | tuned; | changeset | files |
| Fri, 20 Mar 2015 22:35:37 +0100 | wenzelm | tuned; | changeset | files |
| Fri, 20 Mar 2015 22:18:40 +0100 | wenzelm | read instantiations uniformly for rules and tactics; | changeset | files |
| Fri, 20 Mar 2015 21:16:42 +0100 | wenzelm | removed presumably pointless detail; | changeset | files |
| Fri, 20 Mar 2015 20:48:33 +0100 | wenzelm | tuned; | changeset | files |
| Fri, 20 Mar 2015 20:20:21 +0100 | wenzelm | tuned; | changeset | files |
| Fri, 20 Mar 2015 19:05:03 +0100 | wenzelm | make SML/NJ happy; | changeset | files |
| Fri, 20 Mar 2015 16:18:20 +0000 | paulson | Merge | changeset | files |
| Fri, 20 Mar 2015 16:11:28 +0000 | paulson | tweaked a few slow or very ugly proofs | changeset | files |
| Fri, 20 Mar 2015 16:18:28 +0100 | wenzelm | merged | changeset | files |
| Fri, 20 Mar 2015 14:48:04 +0100 | wenzelm | tuned signature; | changeset | files |
| Fri, 20 Mar 2015 11:53:22 +0100 | wenzelm | tuned; | changeset | files |
| Fri, 20 Mar 2015 11:48:34 +0100 | wenzelm | tuned signature; | changeset | files |
| Fri, 20 Mar 2015 11:23:32 +0100 | wenzelm | tuned; | changeset | files |
| Fri, 20 Mar 2015 11:09:08 +0100 | wenzelm | tuned -- prepare instantiation more uniformly; | changeset | files |
| Fri, 20 Mar 2015 14:06:15 +0000 | paulson | Merge | changeset | files |
| Fri, 20 Mar 2015 14:00:22 +0000 | paulson | fixed crash in cancel_numeral_simprocs. NB they still don't work except for type nat! | changeset | files |
| Thu, 19 Mar 2015 22:31:23 +0100 | wenzelm | merged | changeset | files |
| Thu, 19 Mar 2015 22:30:57 +0100 | wenzelm | more position information; | changeset | files |
| Thu, 19 Mar 2015 17:25:57 +0100 | wenzelm | misc tuning; | changeset | files |
| Thu, 19 Mar 2015 15:24:40 +0100 | wenzelm | tuned; | changeset | files |
| Thu, 19 Mar 2015 14:25:32 +0000 | paulson | Merge | changeset | files |
| Thu, 19 Mar 2015 14:24:51 +0000 | paulson | New material for complex sin, cos, tan, Ln, also some reorganisation | changeset | files |
| Thu, 19 Mar 2015 12:36:55 +0100 | wenzelm | updated to sumatra_pdf-3.0; | changeset | files |
| Thu, 19 Mar 2015 11:54:20 +0100 | wenzelm | tuned comments; | changeset | files |
| Thu, 19 Mar 2015 11:13:54 +0100 | wenzelm | slightly more formal historic examples; | changeset | files |
| Wed, 18 Mar 2015 21:40:21 +0100 | traytel | bounded powerset | changeset | files |
| Wed, 18 Mar 2015 17:23:22 +0000 | paulson | new HOL Light material about exp, sin, cos | changeset | files |
| Wed, 18 Mar 2015 14:55:17 +0000 | paulson | new file for complex transcendental functions | changeset | files |
| Wed, 18 Mar 2015 14:30:12 +0000 | paulson | Merge | changeset | files |
| Wed, 18 Mar 2015 14:28:40 +0000 | paulson | Merge | changeset | files |
| Wed, 18 Mar 2015 14:14:07 +0000 | paulson | Merge | changeset | files |
| Wed, 18 Mar 2015 14:13:27 +0000 | paulson | Lots of new material on complex-valued functions. Modified simplification of (x/n)^k | changeset | files |
| 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 |