| Mon, 20 Mar 2023 10:59:27 +0100 |
wenzelm |
clarified operations for ML object sizes;
|
file |
diff |
annotate
|
| Fri, 17 Mar 2023 13:56:54 +0100 |
desharna |
added lemma multp_repeat_mset_repeat_msetI
|
file |
diff |
annotate
|
| Thu, 16 Mar 2023 17:12:06 +0100 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Thu, 16 Mar 2023 15:16:17 +0100 |
wenzelm |
more thorough treatment of build prefs, guarded by system option "build_through": avoid accidental rebuild of HOL etc.;
|
file |
diff |
annotate
|
| Thu, 16 Mar 2023 13:18:25 +0100 |
wenzelm |
clarified build options;
|
file |
diff |
annotate
|
| Thu, 16 Mar 2023 13:37:49 +0100 |
nipkow |
merge conflict
|
file |
diff |
annotate
|
| Thu, 16 Mar 2023 08:30:00 +0100 |
nipkow |
unified function update and map update syntaxes
|
file |
diff |
annotate
|
| Wed, 15 Mar 2023 13:01:57 +0100 |
nipkow |
map update syntax
|
file |
diff |
annotate
|
| Sat, 11 Mar 2023 14:19:09 +0100 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Tue, 07 Mar 2023 23:02:52 +0100 |
wenzelm |
renamed "isabelle build_docker" to "isabelle docker_build" (unrelated to "isabelle build");
|
file |
diff |
annotate
|
| Tue, 07 Mar 2023 22:17:47 +0100 |
wenzelm |
renamed "isabelle log" to "isabelle build_log";
|
file |
diff |
annotate
|
| Sun, 05 Mar 2023 16:14:48 +0100 |
wenzelm |
clarified protocol for "verbose" messages;
|
file |
diff |
annotate
|
| Thu, 02 Mar 2023 17:46:29 +0100 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Thu, 02 Mar 2023 16:09:22 +0100 |
wenzelm |
clarified names;
|
file |
diff |
annotate
|
| Thu, 02 Mar 2023 11:34:54 +0000 |
paulson |
merged
|
file |
diff |
annotate
|
| Tue, 28 Feb 2023 16:46:56 +0000 |
paulson |
Imported a theorem about Infinite_Sum. Importing this theory a bit earlier is causing syntactic ambiguities with Infinite_Set_Sum however; no_notation needed
|
file |
diff |
annotate
|
| Wed, 01 Mar 2023 08:00:51 +0100 |
blanchet |
adopt terminology suggested by Larry Paulson
|
file |
diff |
annotate
|
| Wed, 01 Mar 2023 08:00:51 +0100 |
blanchet |
updated documentation
|
file |
diff |
annotate
|
| Thu, 23 Feb 2023 22:04:32 +0100 |
nipkow |
Map.empty no longer output abbreviation; %_. None is shorter and requires no explanation
|
file |
diff |
annotate
|
| Thu, 23 Feb 2023 15:37:17 +0100 |
desharna |
added lemmas strict_subset_implies_multpDM and strict_subset_implies_multpHO
|
file |
diff |
annotate
|
| Thu, 23 Feb 2023 12:35:37 +0100 |
desharna |
added lemma multpDM_plus_plusI[simp]
|
file |
diff |
annotate
|
| Thu, 23 Feb 2023 12:31:46 +0100 |
desharna |
added lemmas multpDM_mono_strong and multpHO_mono_strong
|
file |
diff |
annotate
|
| Mon, 20 Feb 2023 13:59:42 +0100 |
nipkow |
merged
|
file |
diff |
annotate
|
| Mon, 20 Feb 2023 13:37:51 +0100 |
nipkow |
Backed out changeset 1fde0e4fd791
|
file |
diff |
annotate
|
| Sat, 18 Feb 2023 20:34:09 +0100 |
desharna |
added lemmas asymp_not_liftable_to_multpHO and asymp_multpHO
|
file |
diff |
annotate
|
| Wed, 15 Feb 2023 10:56:23 +0100 |
blanchet |
added refute mode to Sledgehammer to find 'counterexamples'
|
file |
diff |
annotate
|
| Tue, 14 Feb 2023 09:36:35 +0100 |
nipkow |
merged
|
file |
diff |
annotate
|
| Tue, 14 Feb 2023 09:36:06 +0100 |
nipkow |
Map.map_of movement
|
file |
diff |
annotate
|
| Mon, 13 Feb 2023 19:40:38 +0100 |
blanchet |
updated NEWS
|
file |
diff |
annotate
|
| Mon, 30 Jan 2023 15:02:38 +0100 |
wenzelm |
observe option "show_states" in headless server (see also 951abf9db857);
|
file |
diff |
annotate
|