| Tue, 28 Jul 2015 23:14:40 +0200 | wenzelm | clarified context; | changeset | files |
| Tue, 28 Jul 2015 21:47:03 +0200 | wenzelm | more explicit context; | changeset | files |
| Tue, 28 Jul 2015 21:31:16 +0200 | wenzelm | eliminated dead code; | changeset | files |
| Tue, 28 Jul 2015 21:10:41 +0200 | wenzelm | clarified Variable.gen_all; | changeset | files |
| Tue, 28 Jul 2015 20:59:39 +0200 | wenzelm | more explicit context; | changeset | files |
| Tue, 28 Jul 2015 20:15:19 +0200 | wenzelm | more direct access to atomic cterms; | changeset | files |
| Tue, 28 Jul 2015 20:07:05 +0200 | wenzelm | clarified context; | changeset | files |
| Tue, 28 Jul 2015 20:05:53 +0200 | wenzelm | proper context; | changeset | files |
| Tue, 28 Jul 2015 19:49:54 +0200 | wenzelm | more direct access to atomic cterms; | changeset | files |
| Tue, 28 Jul 2015 18:59:15 +0200 | wenzelm | clarified context; | changeset | files |
| Tue, 28 Jul 2015 18:57:47 +0200 | wenzelm | clarified context; | changeset | files |
| Tue, 28 Jul 2015 18:57:10 +0200 | wenzelm | clarified context; | changeset | files |
| Tue, 28 Jul 2015 18:45:32 +0200 | immler | merged | changeset | files |
| Tue, 28 Jul 2015 17:46:35 +0200 | immler | merged | changeset | files |
| Tue, 28 Jul 2015 16:34:08 +0200 | immler | added theory Uniform_Limit | changeset | files |
| Tue, 28 Jul 2015 18:27:39 +0200 | wenzelm | evade timeout problem on macbroy6 (potentially due to NFS oddities); | changeset | files |
| Tue, 28 Jul 2015 17:15:01 +0100 | paulson | tweaks. Got rid of a really slow step | changeset | files |
| Tue, 28 Jul 2015 16:16:13 +0100 | paulson | the Cauchy integral theorem and related material | changeset | files |
| Tue, 28 Jul 2015 13:00:54 +0200 | nipkow | depth -> height; removed del_rightmost (too specifi) | changeset | files |
| Mon, 27 Jul 2015 23:56:11 +0200 | wenzelm | tuned; | changeset | files |
| Mon, 27 Jul 2015 23:41:57 +0200 | wenzelm | merged | changeset | files |
| Mon, 27 Jul 2015 23:40:39 +0200 | wenzelm | tuned signature; | changeset | files |
| Mon, 27 Jul 2015 22:44:02 +0200 | haftmann | formal class for factorial (semi)rings | changeset | files |
| Mon, 27 Jul 2015 22:08:46 +0200 | wenzelm | merged | changeset | files |
| Mon, 27 Jul 2015 17:56:08 +0200 | wenzelm | NEWS; | changeset | files |
| Mon, 27 Jul 2015 17:44:55 +0200 | wenzelm | tuned signature; | changeset | files |
| Mon, 27 Jul 2015 16:52:57 +0100 | paulson | New material for Cauchy's integral theorem | changeset | files |
| Mon, 27 Jul 2015 16:35:12 +0200 | wenzelm | tuned signature for print_nested_cases; | changeset | files |
| Mon, 27 Jul 2015 15:13:05 +0200 | wenzelm | more explicit checks -- improved errors; | changeset | files |
| Mon, 27 Jul 2015 14:56:06 +0200 | wenzelm | eliminated cterm_instantiate; | changeset | files |
| Mon, 27 Jul 2015 14:55:26 +0200 | wenzelm | updated to infer_instantiate; | changeset | files |
| Mon, 27 Jul 2015 11:30:10 +0200 | wenzelm | tuned signature; | changeset | files |
| Mon, 27 Jul 2015 00:17:18 +0200 | wenzelm | added infer_instantiate_vars, which allows inconsistent types for variables, as required for Metis proof reconstruction; | changeset | files |
| Sun, 26 Jul 2015 22:26:11 +0200 | wenzelm | eliminated atac, rtac, etac, dtac, ftac; | changeset | files |
| Sun, 26 Jul 2015 22:19:14 +0200 | wenzelm | updated to infer_instantiate; | changeset | files |
| Sun, 26 Jul 2015 22:07:37 +0200 | wenzelm | updated to infer_instantiate; | changeset | files |
| Sun, 26 Jul 2015 21:50:44 +0200 | wenzelm | updated to infer_instantiate; | changeset | files |
| Sun, 26 Jul 2015 21:48:00 +0200 | wenzelm | proper context; | changeset | files |
| Sun, 26 Jul 2015 20:57:35 +0200 | wenzelm | updated to infer_instantiate; | changeset | files |
| Sun, 26 Jul 2015 20:56:44 +0200 | wenzelm | updated to infer_instantiate; | changeset | files |
| Sun, 26 Jul 2015 20:54:02 +0200 | wenzelm | ignore non-existant variables, like other instantiate rules; | changeset | files |
| Sun, 26 Jul 2015 17:32:59 +0200 | wenzelm | updated to infer_instantiate; | changeset | files |
| Sun, 26 Jul 2015 17:24:54 +0200 | wenzelm | updated to infer_instantiate; | changeset | files |
| Sun, 26 Jul 2015 12:24:16 +0200 | wenzelm | added infer_instantiate'; | changeset | files |
| Sun, 26 Jul 2015 11:08:57 +0200 | wenzelm | more uniform exceptions, like cterm_instantiate; | changeset | files |
| Sat, 25 Jul 2015 23:41:53 +0200 | wenzelm | updated to infer_instantiate; | changeset | files |
| Sat, 25 Jul 2015 23:15:37 +0200 | wenzelm | more accurate maxidx; | changeset | files |
| Sat, 25 Jul 2015 21:54:09 +0200 | wenzelm | clarified error; | changeset | files |
| Sat, 25 Jul 2015 21:37:09 +0200 | wenzelm | added infer_instantiate, which is meant to supersede cterm_instantiate; | changeset | files |
| Fri, 24 Jul 2015 22:29:06 +0200 | wenzelm | eliminated alias; | changeset | files |
| Fri, 24 Jul 2015 22:20:22 +0200 | wenzelm | proper context; | changeset | files |
| Fri, 24 Jul 2015 22:19:36 +0200 | wenzelm | unused; | changeset | files |
| Fri, 24 Jul 2015 22:16:39 +0200 | wenzelm | proper context; | changeset | files |
| Thu, 23 Jul 2015 22:13:42 +0200 | wenzelm | more symbols by default, without xsymbols mode; | changeset | files |
| Thu, 23 Jul 2015 16:40:47 +0200 | hoelzl | Measures form a CCPO | changeset | files |
| Thu, 23 Jul 2015 16:39:10 +0200 | hoelzl | reorganized Extended_Real | changeset | files |
| Thu, 23 Jul 2015 14:25:05 +0200 | wenzelm | isabelle update_cartouches; | changeset | files |
| Thu, 23 Jul 2015 14:20:51 +0200 | wenzelm | tuned proofs; | changeset | files |
| Thu, 23 Jul 2015 13:28:34 +0200 | wenzelm | proper latex; | changeset | files |
| Wed, 22 Jul 2015 23:26:00 +0200 | wenzelm | tuned proofs; | changeset | files |