| Sun, 16 Aug 2015 17:11:31 +0200 | wenzelm | separate type theory_id; | changeset | files |
| Sun, 16 Aug 2015 15:36:06 +0200 | wenzelm | delete precisely the added rules; | changeset | files |
| Sun, 16 Aug 2015 14:48:37 +0200 | wenzelm | clarified context; | changeset | files |
| Sun, 16 Aug 2015 11:55:21 +0200 | wenzelm | tuned whitespace; | changeset | files |
| Sun, 16 Aug 2015 11:46:08 +0200 | wenzelm | tuned signature; | changeset | files |
| Sun, 16 Aug 2015 11:29:06 +0200 | wenzelm | tuned; | changeset | files |
| Sat, 15 Aug 2015 23:10:13 +0200 | wenzelm | tuned whitespace; | changeset | files |
| Sat, 15 Aug 2015 22:47:03 +0200 | wenzelm | tuned whitespace; | changeset | files |
| Sat, 15 Aug 2015 20:27:23 +0200 | wenzelm | obsolete; | changeset | files |
| Sat, 15 Aug 2015 20:07:05 +0200 | wenzelm | clarified context; | changeset | files |
| Sat, 15 Aug 2015 19:42:35 +0200 | wenzelm | clarified context; | changeset | files |
| Sat, 15 Aug 2015 19:11:11 +0200 | wenzelm | tuned GUI; | changeset | files |
| Sat, 15 Aug 2015 19:07:11 +0200 | wenzelm | proper setup of evaluation context; | changeset | files |
| Sat, 15 Aug 2015 19:00:04 +0200 | wenzelm | tuned; | changeset | files |
| Sat, 15 Aug 2015 18:59:31 +0200 | wenzelm | more robust access to stable tip version: take all pending edits into account, don't assume model for current buffer; | changeset | files |
| Sat, 15 Aug 2015 17:38:20 +0200 | wenzelm | allow to break running threads at next possible breakpoint (simplified version of former option, see f3039309702e); | changeset | files |
| Sat, 15 Aug 2015 16:47:52 +0200 | wenzelm | tuned signature; | changeset | files |
| Thu, 13 Aug 2015 15:22:11 +0200 | haftmann | qualified adjust_* | changeset | files |
| Thu, 13 Aug 2015 10:05:58 +0200 | haftmann | more lemmas | changeset | files |
| Thu, 13 Aug 2015 16:47:00 +0200 | traytel | unfold intermediate definitions (stemming from composition) in lifted bnf operations | changeset | files |
| Thu, 13 Aug 2015 13:55:52 +0200 | wenzelm | merged | changeset | files |
| Thu, 13 Aug 2015 13:55:48 +0200 | wenzelm | more standard options; | changeset | files |
| Thu, 13 Aug 2015 11:40:31 +0200 | wenzelm | prefer official @{make_string}; | changeset | files |
| Thu, 13 Aug 2015 11:05:19 +0200 | wenzelm | tuned signature, in accordance to sortBy in Scala; | changeset | files |
| Wed, 12 Aug 2015 21:38:39 +0200 | wenzelm | clarified modules; | changeset | files |
| Thu, 13 Aug 2015 11:14:16 +0200 | traytel | tuned NEWS | changeset | files |
| Wed, 12 Aug 2015 20:46:33 +0200 | traytel | actually process lift_bnf regression suite | changeset | files |
| Wed, 12 Aug 2015 20:46:33 +0200 | traytel | NEWS, CONTRIBUTORS, documentation for lift_bnf | changeset | files |
| Wed, 12 Aug 2015 20:46:33 +0200 | traytel | use lift_bnf in an example | changeset | files |
| Wed, 12 Aug 2015 20:46:33 +0200 | traytel | new command for lifting BNF structure over typedefs | changeset | files |
| Wed, 12 Aug 2015 13:56:46 +0200 | wenzelm | more thorough reload; | changeset | files |
| Wed, 12 Aug 2015 13:53:51 +0200 | wenzelm | resolve undefined blobs by default, e.g. relevant for ML debugger to avoid reset of breakpoints after reload; | changeset | files |
| Wed, 12 Aug 2015 03:07:01 +0200 | wenzelm | merged | changeset | files |
| Wed, 12 Aug 2015 02:40:39 +0200 | wenzelm | tuned colors; | changeset | files |
| Wed, 12 Aug 2015 02:21:00 +0200 | wenzelm | clarified breakpoint rendering; | changeset | files |
| Wed, 12 Aug 2015 02:20:06 +0200 | wenzelm | clarified; | changeset | files |
| Wed, 12 Aug 2015 01:39:31 +0200 | wenzelm | default ML context for forks, e.g. relevant for debugging and toplevel pretty-printing; | changeset | files |
| Wed, 12 Aug 2015 01:25:00 +0200 | wenzelm | clarified init/exit vs. session phase; | changeset | files |
| Wed, 12 Aug 2015 10:15:18 +1000 | Daniel Matichuk | clarify type vs. term instantiation when forming closure; | changeset | files |
| Tue, 11 Aug 2015 22:17:19 +0200 | wenzelm | more accurate dependencies; | changeset | files |
| Tue, 11 Aug 2015 22:11:09 +0200 | wenzelm | tuned; | changeset | files |
| Tue, 11 Aug 2015 22:06:25 +0200 | wenzelm | clarified thread re-selection; | changeset | files |
| Tue, 11 Aug 2015 22:01:11 +0200 | wenzelm | clarified tree row handling; | changeset | files |
| Tue, 11 Aug 2015 21:36:25 +0200 | wenzelm | proper context (amending 7aad4be8a48e); | changeset | files |
| Tue, 11 Aug 2015 21:24:11 +0200 | wenzelm | suppress threads without debug state; | changeset | files |
| Tue, 11 Aug 2015 21:15:29 +0200 | wenzelm | clarified events; | changeset | files |
| Tue, 11 Aug 2015 20:49:22 +0200 | wenzelm | clarified GUI event handling; | changeset | files |
| Tue, 11 Aug 2015 20:32:56 +0200 | wenzelm | tuned signature; | changeset | files |
| Tue, 11 Aug 2015 20:28:11 +0200 | wenzelm | tuned; | changeset | files |
| Tue, 11 Aug 2015 20:21:13 +0200 | wenzelm | misc tuning and clarification; | changeset | files |
| Tue, 11 Aug 2015 20:05:27 +0200 | wenzelm | print values for stack entry; | changeset | files |
| Tue, 11 Aug 2015 18:42:29 +0200 | wenzelm | clarified output; | changeset | files |
| Tue, 11 Aug 2015 18:00:28 +0200 | wenzelm | default ML context for all command transactions, e.g. relevant for debugging and toplevel pretty-printing; | changeset | files |
| Tue, 11 Aug 2015 17:06:23 +0200 | wenzelm | clarified break *point* position; | changeset | files |
| Tue, 11 Aug 2015 17:00:16 +0200 | wenzelm | support hyperlinks with optional focus change; | changeset | files |
| Tue, 11 Aug 2015 15:24:49 +0200 | wenzelm | tuned; | changeset | files |
| Tue, 11 Aug 2015 14:35:08 +0200 | wenzelm | vacuous input means continue, e.g. after exit; | changeset | files |
| Tue, 11 Aug 2015 14:21:00 +0200 | wenzelm | GUI actions depend on active debugger; | changeset | files |
| Tue, 11 Aug 2015 14:13:36 +0200 | wenzelm | init/exit depending on active debugger panels; | changeset | files |
| Tue, 11 Aug 2015 13:50:59 +0200 | wenzelm | eliminated cancel operation: disrupts normal evaluation of thread; | changeset | files |
| Tue, 11 Aug 2015 11:55:41 +0200 | wenzelm | register thread such that cancel works; | changeset | files |
| Mon, 10 Aug 2015 22:34:00 +0200 | wenzelm | clarified default selection; | changeset | files |
| Mon, 10 Aug 2015 22:21:55 +0200 | wenzelm | report final debugger_state more robustly, e.g. after interrupt; | changeset | files |
| Mon, 10 Aug 2015 21:11:15 +0200 | wenzelm | eliminated global option: breakpoints control this individually; | changeset | files |
| Mon, 10 Aug 2015 21:06:10 +0200 | wenzelm | more uniform ScrollPane, like graphview; | changeset | files |
| Mon, 10 Aug 2015 20:42:59 +0200 | wenzelm | tuned signature; | changeset | files |
| Mon, 10 Aug 2015 20:25:04 +0200 | wenzelm | tuned rendering; | changeset | files |
| Mon, 10 Aug 2015 20:22:49 +0200 | wenzelm | set breakpoint state on ML side, relying on stable situation within the PIDE editing queue; | changeset | files |
| Mon, 10 Aug 2015 19:17:49 +0200 | wenzelm | more thorough Encode.string; | changeset | files |
| Mon, 10 Aug 2015 17:49:36 +0200 | wenzelm | added action to toggle breakpoints (on editor side); | changeset | files |
| Mon, 10 Aug 2015 16:14:50 +0200 | wenzelm | sort lines; | changeset | files |
| Mon, 10 Aug 2015 16:05:41 +0200 | wenzelm | rendering for debugger/breakpoint active state; | changeset | files |
| Mon, 10 Aug 2015 14:14:49 +0200 | wenzelm | follow debugger focus; | changeset | files |
| Mon, 10 Aug 2015 14:13:49 +0200 | wenzelm | tuned signature; | changeset | files |
| Mon, 10 Aug 2015 13:54:12 +0200 | wenzelm | tuned imports; | changeset | files |
| Mon, 10 Aug 2015 11:23:49 +0200 | wenzelm | tuned messages; | changeset | files |
| Mon, 10 Aug 2015 11:20:16 +0200 | wenzelm | clarified ML options; | changeset | files |
| Sat, 08 Aug 2015 22:08:43 +0200 | wenzelm | merged | changeset | files |
| Sat, 08 Aug 2015 21:33:11 +0200 | wenzelm | more single stepping; | changeset | files |
| Sat, 08 Aug 2015 10:51:33 +0200 | haftmann | direct bootstrap of integer division from natural division | changeset | files |
| Thu, 06 Aug 2015 23:56:48 +0200 | haftmann | slight cleanup of lemmas | changeset | files |
| Thu, 06 Aug 2015 19:12:09 +0200 | haftmann | obsolete since no code generator without dictionary construction left | changeset | files |
| Fri, 07 Aug 2015 17:58:12 +0200 | wenzelm | make SML/NJ work; | changeset | files |
| Fri, 07 Aug 2015 16:15:53 +0200 | wenzelm | suppress empty messages as usual; | changeset | files |
| Fri, 07 Aug 2015 14:55:35 +0200 | wenzelm | proper Symbol.decode/encode; | changeset | files |
| Fri, 07 Aug 2015 14:46:56 +0200 | wenzelm | eval ML context; | changeset | files |
| Fri, 07 Aug 2015 11:44:11 +0200 | wenzelm | maintain history more often; | changeset | files |
| Thu, 06 Aug 2015 23:20:15 +0200 | wenzelm | approximate old selection after update; | changeset | files |
| Thu, 06 Aug 2015 23:08:42 +0200 | wenzelm | expand all rows for robustness and simplicity; | changeset | files |
| Thu, 06 Aug 2015 21:31:54 +0200 | wenzelm | evaluate ML expressions within debugger context; | changeset | files |
| Thu, 06 Aug 2015 20:33:12 +0200 | wenzelm | clarified debugger loop; | changeset | files |
| Thu, 06 Aug 2015 17:40:05 +0200 | wenzelm | clarified thread state; | changeset | files |
| Thu, 06 Aug 2015 14:29:05 +0200 | wenzelm | tuned; | changeset | files |
| Thu, 06 Aug 2015 14:28:59 +0200 | wenzelm | more controls; | changeset | files |
| Thu, 06 Aug 2015 14:23:59 +0200 | wenzelm | tuned; | changeset | files |
| Thu, 06 Aug 2015 11:46:47 +0200 | wenzelm | clarified signature, to make debugger.ML compile with current official ML versions; | changeset | files |
| Wed, 05 Aug 2015 21:46:52 +0200 | wenzelm | support for tree selection; | changeset | files |
| Wed, 05 Aug 2015 20:36:07 +0200 | wenzelm | proper dynamic update; | changeset | files |
| Wed, 05 Aug 2015 20:19:51 +0200 | wenzelm | tuned; | changeset | files |
| Wed, 05 Aug 2015 20:04:21 +0200 | wenzelm | more GUI components; | changeset | files |
| Wed, 05 Aug 2015 20:03:22 +0200 | wenzelm | tuned; | changeset | files |
| Wed, 05 Aug 2015 20:02:44 +0200 | wenzelm | tuned; | changeset | files |
| Wed, 05 Aug 2015 16:22:56 +0200 | wenzelm | more controls; | changeset | files |
| Wed, 05 Aug 2015 16:22:40 +0200 | wenzelm | proper initialization; | changeset | files |
| Wed, 05 Aug 2015 16:13:42 +0200 | wenzelm | tuned signature; | changeset | files |
| Wed, 05 Aug 2015 14:18:07 +0200 | wenzelm | protocol support for thread debugger state; | changeset | files |
| Tue, 04 Aug 2015 23:11:16 +0200 | wenzelm | eliminated clone; | changeset | files |
| Tue, 04 Aug 2015 15:00:58 +0200 | wenzelm | merged | changeset | files |
| Tue, 04 Aug 2015 14:29:45 +0200 | wenzelm | more symbols; | changeset | files |
| Tue, 04 Aug 2015 14:06:24 +0200 | wenzelm | more symbols; | changeset | files |
| Tue, 04 Aug 2015 12:19:41 +0200 | traytel | more documentation of coercions | changeset | files |
| Thu, 30 Jul 2015 21:56:19 +0200 | wenzelm | merged | changeset | files |
| Thu, 30 Jul 2015 14:02:19 +0200 | wenzelm | clarified management of (single) session; | changeset | files |
| Thu, 30 Jul 2015 11:39:30 +0200 | wenzelm | maintain debugger output messages; | changeset | files |
| Thu, 30 Jul 2015 11:32:58 +0200 | wenzelm | provide CharSequence operations as well; | changeset | files |
| Wed, 29 Jul 2015 15:52:57 +0200 | wenzelm | more GUI components; | changeset | files |
| Wed, 29 Jul 2015 14:04:19 +0200 | wenzelm | tuned; | changeset | files |
| Wed, 29 Jul 2015 13:34:04 +0200 | wenzelm | separate channel for debugger output; | changeset | files |
| Wed, 29 Jul 2015 11:41:26 +0200 | wenzelm | clarified thread name; | changeset | files |
| Thu, 30 Jul 2015 09:49:43 +0200 | Andreas Lochbihler | add coinduction rule for infinite | changeset | files |
| Tue, 28 Jul 2015 23:29:13 +0200 | wenzelm | merged | changeset | files |
| 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 |
| Wed, 22 Jul 2015 14:55:42 +0200 | wenzelm | tuned proofs; | changeset | files |
| Tue, 21 Jul 2015 19:04:36 +0200 | wenzelm | support for ML debugger; | changeset | files |
| Tue, 21 Jul 2015 14:12:45 +0200 | wenzelm | more explicit thread identification; | changeset | files |
| Tue, 21 Jul 2015 14:07:06 +0200 | wenzelm | avoid lxbroy2, lxbroy3, lxbroy4, which are often busy with other processes; | changeset | files |
| Mon, 20 Jul 2015 23:12:50 +0100 | paulson | new material for multivariate analysis, etc. | changeset | files |
| Mon, 20 Jul 2015 11:40:43 +0200 | wenzelm | proper LaTeX; | changeset | files |
| Sun, 19 Jul 2015 21:16:39 +0200 | wenzelm | updated to jdk-8u51; | changeset | files |
| Sun, 19 Jul 2015 00:03:10 +0200 | wenzelm | more symbols; | changeset | files |
| Sat, 18 Jul 2015 22:58:50 +0200 | wenzelm | isabelle update_cartouches; | changeset | files |
| Sat, 18 Jul 2015 21:44:18 +0200 | wenzelm | prefer tactics with explicit context; | changeset | files |
| Sat, 18 Jul 2015 21:25:55 +0200 | wenzelm | prefer tactics with explicit context; | changeset | files |
| Sat, 18 Jul 2015 20:59:51 +0200 | wenzelm | merged | changeset | files |
| Sat, 18 Jul 2015 20:54:56 +0200 | wenzelm | prefer tactics with explicit context; | changeset | files |
| Sat, 18 Jul 2015 20:53:05 +0200 | wenzelm | tuned whitespace; | changeset | files |
| Sat, 18 Jul 2015 20:47:08 +0200 | wenzelm | prefer tactics with explicit context; | changeset | files |
| Sat, 18 Jul 2015 20:37:16 +0200 | wenzelm | reactivated dead code; | changeset | files |
| Fri, 17 Jul 2015 21:45:15 +0200 | wenzelm | more uniform ComponentAdapter; | changeset | files |
| Fri, 17 Jul 2015 21:40:47 +0200 | wenzelm | skeleton for interactive debugger; | changeset | files |
| Fri, 17 Jul 2015 21:37:33 +0200 | wenzelm | tuned; | changeset | files |
| Fri, 17 Jul 2015 21:00:41 +0200 | wenzelm | tuned; | changeset | files |
| Fri, 17 Jul 2015 17:17:39 +0200 | wenzelm | store breakpoints within ML environment; | changeset | files |
| Fri, 17 Jul 2015 16:43:53 +0200 | wenzelm | clarified ML compiler parameters: always provide PolyML.Compiler.CPDebug, ignore global default; | changeset | files |
| Fri, 17 Jul 2015 16:23:25 +0200 | wenzelm | report possible breakpoint positions; | changeset | files |
| Fri, 17 Jul 2015 16:03:11 +0200 | wenzelm | proper attribute; | changeset | files |
| Fri, 17 Jul 2015 16:13:03 +0200 | traytel | forgotten selector | changeset | files |
| Thu, 16 Jul 2015 18:36:16 +0200 | blanchet | made code less loopy | changeset | files |
| Thu, 16 Jul 2015 17:47:49 +0200 | blanchet | keep smart default for Isar proofs in Sledgehammer panel (if the option is not checked) | changeset | files |
| Thu, 16 Jul 2015 17:38:36 +0200 | blanchet | generalized generic translation function | changeset | files |
| Thu, 16 Jul 2015 17:36:38 +0200 | blanchet | merge | changeset | files |
| Thu, 16 Jul 2015 17:25:48 +0200 | blanchet | tuning | changeset | files |
| Thu, 16 Jul 2015 17:25:44 +0200 | blanchet | generalized limitation in documentation | changeset | files |
| Thu, 16 Jul 2015 17:25:44 +0200 | blanchet | made tactic more robust w.r.t. equations containing 'case_prod' | changeset | files |
| Thu, 16 Jul 2015 17:02:07 +0200 | wenzelm | merged | changeset | files |
| Thu, 16 Jul 2015 16:32:37 +0200 | wenzelm | merged | changeset | files |
| Thu, 16 Jul 2015 16:30:43 +0200 | wenzelm | clarified boundary cases of completion; | changeset | files |
| Thu, 16 Jul 2015 14:40:23 +0200 | wenzelm | additional ML parse tree components for Poly/ML 5.5.3, or later; | changeset | files |
| Thu, 16 Jul 2015 11:38:18 +0200 | wenzelm | added option ML_debugger; | changeset | files |
| Thu, 16 Jul 2015 11:10:57 +0200 | wenzelm | ML debugger interface; | changeset | files |
| Thu, 16 Jul 2015 12:23:22 +0200 | traytel | {r,e,d,f}tac with proper context in BNF | changeset | files |
| Thu, 16 Jul 2015 10:48:20 +0200 | hoelzl | move disjoint sets to their own theory | changeset | files |
| Wed, 15 Jul 2015 11:25:51 +0200 | wenzelm | back to uniform BUILD_ARGS: first some options, then some sessions (cf. 4fce5d462afc); | changeset | files |
| Tue, 14 Jul 2015 19:08:40 +0200 | wenzelm | merged | changeset | files |
| Tue, 14 Jul 2015 19:08:27 +0200 | wenzelm | more explicit command-line option for isabelle build; | changeset | files |
| Tue, 14 Jul 2015 19:01:46 +0200 | wenzelm | more aggressive compaction of multi-goal proof terms (see also a8babbb6d5ea, 4dd0ba632e40); | changeset | files |
| Tue, 14 Jul 2015 11:29:43 +0200 | wenzelm | normalize proof before splitting conjunctions, according to Proof.conclude_goal (see also 4dd0ba632e40) -- may reduce general resource usage; | changeset | files |
| Tue, 14 Jul 2015 13:48:03 +0200 | hoelzl | generalized filtermap_homeomorph to filtermap_fun_inverse; add eventually_at_top/bot_not_equal | changeset | files |
| Tue, 14 Jul 2015 13:37:44 +0200 | hoelzl | add continuous_onI_mono | changeset | files |
| Mon, 13 Jul 2015 19:25:58 +0200 | blanchet | tuned description | changeset | files |
| Mon, 13 Jul 2015 19:22:55 +0200 | blanchet | tuning | changeset | files |
| Mon, 13 Jul 2015 19:22:50 +0200 | blanchet | updated Isabelle description to CASC | changeset | files |
| Mon, 13 Jul 2015 16:54:27 +0200 | blanchet | imported patch up_casc | changeset | files |
| Mon, 13 Jul 2015 14:40:16 +0200 | hoelzl | add emeasure_add_AE | changeset | files |
| Mon, 13 Jul 2015 14:39:50 +0200 | hoelzl | stronger induction assumption in lfp_transfer and emeasure_lfp | changeset | files |
| Mon, 13 Jul 2015 11:05:50 +0200 | wenzelm | refrain from testing HOL-Proofs for x86_64-linux: takes more than 4h; | changeset | files |
| Sun, 12 Jul 2015 13:04:42 +0200 | Lars Hupel | Quickcheck setup for finite sets | changeset | files |
| Sat, 11 Jul 2015 21:32:06 +0200 | wenzelm | tuned proofs; | changeset | files |
| Sat, 11 Jul 2015 00:14:54 +0200 | wenzelm | tuned proofs; | changeset | files |
| Thu, 09 Jul 2015 23:48:55 +0200 | wenzelm | merged | changeset | files |
| Thu, 09 Jul 2015 23:46:21 +0200 | wenzelm | tuned proofs; | changeset | files |