| Tue, 21 Jan 2025 11:17:05 +0100 | Fabian Huch | merged | changeset | files |
| Tue, 21 Jan 2025 11:15:34 +0100 | Fabian Huch | clarified: more operations; | changeset | files |
| Tue, 21 Jan 2025 11:14:00 +0100 | Fabian Huch | tuned default nightly start: less events at 00:17:00; | changeset | files |
| Tue, 21 Jan 2025 11:12:44 +0100 | Fabian Huch | use cycles in ci triggers; | changeset | files |
| Tue, 21 Jan 2025 10:05:40 +0100 | Fabian Huch | varying-length calendar cycles, e.g. for ci jobs every week on a certain day/time; | changeset | files |
| Mon, 20 Jan 2025 09:17:37 +0100 | Fabian Huch | clarified; | changeset | files |
| Fri, 17 Jan 2025 13:43:16 +0100 | Fabian Huch | tuned whitespace; | changeset | files |
| Thu, 16 Jan 2025 19:00:29 +0100 | Fabian Huch | add find_facts_index command to use within Isabelle/Scala; | changeset | files |
| Thu, 16 Jan 2025 18:37:23 +0100 | Fabian Huch | clarified: add afp_root argument; | changeset | files |
| Mon, 20 Jan 2025 22:20:14 +0100 | nipkow | merged | changeset | files |
| Mon, 20 Jan 2025 22:19:54 +0100 | nipkow | introduced/overloaded power operator ^^ lists | changeset | files |
| 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 |