| Mon, 20 Jan 2025 22:15:11 +0100 |
haftmann |
systematic checks for bit operations and more rules on symbolic terms
|
changeset |
files
|
| Mon, 20 Jan 2025 22:15:11 +0100 |
haftmann |
explicitly report dependencies on missing code equations
|
changeset |
files
|
| Sun, 19 Jan 2025 18:18:07 +0000 |
paulson |
simplified old proofs
|
changeset |
files
|
| Fri, 17 Jan 2025 23:00:13 +0000 |
paulson |
merged
|
changeset |
files
|
| Fri, 17 Jan 2025 20:24:09 +0000 |
paulson |
merged
|
changeset |
files
|
| Fri, 17 Jan 2025 20:24:02 +0000 |
paulson |
A variety of tweaks
|
changeset |
files
|
| Fri, 17 Jan 2025 23:15:47 +0100 |
wenzelm |
avoid legacy warnings in "test_code check in OCaml";
|
changeset |
files
|
| Fri, 17 Jan 2025 23:10:39 +0100 |
wenzelm |
proper condition for strict "test_code check in OCaml" and "test_code check in GHC";
|
changeset |
files
|
| Fri, 17 Jan 2025 22:38:15 +0100 |
wenzelm |
more NEWS;
|
changeset |
files
|
| Fri, 17 Jan 2025 21:30:08 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 17 Jan 2025 20:30:01 +0100 |
wenzelm |
misc tuning;
|
changeset |
files
|
| Fri, 17 Jan 2025 19:56:34 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 17 Jan 2025 19:46:36 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 17 Jan 2025 19:40:56 +0100 |
wenzelm |
clarified pattern matching;
|
changeset |
files
|
| Fri, 17 Jan 2025 19:30:26 +0100 |
wenzelm |
misc tuning;
|
changeset |
files
|
| Fri, 17 Jan 2025 17:01:43 +0100 |
wenzelm |
misc tuning and clarification;
|
changeset |
files
|
| Fri, 17 Jan 2025 16:49:01 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 17 Jan 2025 16:22:49 +0100 |
wenzelm |
clarified exceptions and messages: use "error" only for user-errors, not system failures;
|
changeset |
files
|
| Fri, 17 Jan 2025 16:13:48 +0100 |
wenzelm |
minor performance tuning: more elementary operations;
|
changeset |
files
|
| Fri, 17 Jan 2025 16:03:35 +0100 |
wenzelm |
minor performance tuning;
|
changeset |
files
|
| Fri, 17 Jan 2025 15:39:40 +0100 |
wenzelm |
clarified inst_type: more direct Thm.instantiate_frees;
|
changeset |
files
|
| Fri, 17 Jan 2025 14:47:25 +0100 |
wenzelm |
more direct Thm.free: avoid re-certification;
|
changeset |
files
|
| Fri, 17 Jan 2025 14:31:48 +0100 |
wenzelm |
clarified signature: more explicit types;
|
changeset |
files
|
| Fri, 17 Jan 2025 13:44:45 +0100 |
wenzelm |
tuned names;
|
changeset |
files
|
| Fri, 17 Jan 2025 13:04:34 +0100 |
wenzelm |
tuned names;
|
changeset |
files
|
| Fri, 17 Jan 2025 13:00:39 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Fri, 17 Jan 2025 12:50:46 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 17 Jan 2025 12:46:50 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Fri, 17 Jan 2025 12:41:01 +0100 |
wenzelm |
clarified signature: more standard Isabelle/ML;
|
changeset |
files
|
| Fri, 17 Jan 2025 12:19:11 +0100 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Fri, 17 Jan 2025 12:10:59 +0100 |
wenzelm |
more robust import_file path: proper master_directory;
|
changeset |
files
|
| Fri, 17 Jan 2025 11:49:31 +0100 |
wenzelm |
tuned signature: more operations;
|
changeset |
files
|
| Fri, 17 Jan 2025 11:47:47 +0100 |
wenzelm |
unused;
|
changeset |
files
|
| Fri, 17 Jan 2025 11:24:40 +0100 |
wenzelm |
tuned signature, following Isabelle/Scala;
|
changeset |
files
|
| Fri, 17 Jan 2025 11:16:11 +0100 |
wenzelm |
clarified signature, following Isabelle/Scala;
|
changeset |
files
|
| Fri, 17 Jan 2025 11:05:36 +0100 |
wenzelm |
clarified pattern via antiquotations;
|
changeset |
files
|
| Fri, 17 Jan 2025 11:01:44 +0100 |
wenzelm |
misc tuning and clarification;
|
changeset |
files
|
| Fri, 17 Jan 2025 10:56:10 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 17 Jan 2025 10:53:30 +0100 |
wenzelm |
clarified make_type: proper make_name;
|
changeset |
files
|
| Fri, 17 Jan 2025 10:51:47 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 17 Jan 2025 10:46:59 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 17 Jan 2025 10:43:23 +0100 |
wenzelm |
clarified signature: more standard Isabelle/ML;
|
changeset |
files
|
| Thu, 16 Jan 2025 23:20:44 +0100 |
wenzelm |
reproducible construction of HOL Light export bundle;
|
changeset |
files
|
| Thu, 16 Jan 2025 22:54:25 +0100 |
wenzelm |
tuned messages;
|
changeset |
files
|
| Thu, 16 Jan 2025 22:48:16 +0100 |
wenzelm |
more robust options;
|
changeset |
files
|
| Thu, 16 Jan 2025 13:14:24 +0100 |
wenzelm |
clarified signature: more explicit operations;
|
changeset |
files
|
| Thu, 16 Jan 2025 12:45:48 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 16 Jan 2025 12:41:55 +0100 |
wenzelm |
tuned: prefer inlined thms;
|
changeset |
files
|
| Thu, 16 Jan 2025 12:12:32 +0100 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Thu, 16 Jan 2025 11:55:20 +0100 |
wenzelm |
proper GUI.Style_HTML.make_text, e.g. for term "x < y";
|
changeset |
files
|
| Wed, 15 Jan 2025 15:49:16 +0100 |
wenzelm |
clarified signature: more explicit operations;
|
changeset |
files
|
| Wed, 15 Jan 2025 15:13:39 +0100 |
wenzelm |
provide less ambitious "isabelle ocaml_setup_base", notably for platforms without gmp-dev;
|
changeset |
files
|
| Wed, 15 Jan 2025 13:45:22 +0100 |
wenzelm |
clarified signature: more explicit operations;
|
changeset |
files
|
| Tue, 14 Jan 2025 11:34:17 +0100 |
wenzelm |
update to ocaml-base-compiler.4.14.1, which coincides with ocaml on Ubuntu 24.04;
|
changeset |
files
|
| Fri, 17 Jan 2025 12:17:37 +0100 |
Fabian Huch |
isabelle_id: report sync id, if available;
|
changeset |
files
|
| Fri, 17 Jan 2025 12:16:52 +0100 |
Fabian Huch |
clarified: sync_id operation, similar to archive_id;
|
changeset |
files
|
| Thu, 16 Jan 2025 16:10:26 +0100 |
Fabian Huch |
build schedule: limit history length;
|
changeset |
files
|
| Thu, 16 Jan 2025 15:38:10 +0100 |
Fabian Huch |
tuned whitespace;
|
changeset |
files
|
| Thu, 16 Jan 2025 18:07:31 +0100 |
haftmann |
restrict check to PolyML
|
changeset |
files
|
| Thu, 16 Jan 2025 10:09:42 +0000 |
paulson |
merged
|
changeset |
files
|