| Sat, 18 Jan 2025 17:22:08 +0100 |
wenzelm |
move material from https://gitlab.inria.fr/hol-light-isabelle/hol-light 72b2b702eadb and https://gitlab.inria.fr/hol-light-isabelle/import ce58755b0232 into Isabelle repository: results from running "isabelle component_hol_light_import" of previous version;
|
changeset |
files
|
| Sat, 18 Jan 2025 16:26:43 +0100 |
wenzelm |
original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
|
changeset |
files
|
| Sat, 18 Jan 2025 13:20:47 +0100 |
wenzelm |
tuned names;
|
changeset |
files
|
| Sat, 18 Jan 2025 13:10:09 +0100 |
wenzelm |
misc cleanup and minor performance tuning;
|
changeset |
files
|
| Sat, 18 Jan 2025 12:53:23 +0100 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Sat, 18 Jan 2025 12:45:33 +0100 |
wenzelm |
tuned: prefer existing operations;
|
changeset |
files
|
| Sat, 18 Jan 2025 12:43:24 +0100 |
wenzelm |
tuned source structure;
|
changeset |
files
|
| Sat, 18 Jan 2025 12:25:23 +0100 |
wenzelm |
tuned state operations;
|
changeset |
files
|
| Sat, 18 Jan 2025 12:08:13 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Sat, 18 Jan 2025 12:05:56 +0100 |
wenzelm |
misc tuning and clarification: prefer state operations, avoid redundant ctyp_of/cterm_of;
|
changeset |
files
|
| Sat, 18 Jan 2025 11:09:00 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 18 Jan 2025 11:03:18 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 18 Jan 2025 10:59:00 +0100 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Thu, 23 Jan 2025 13:42:58 +0100 |
Fabian Huch |
merged
|
changeset |
files
|
| Wed, 22 Jan 2025 15:05:29 +0100 |
Fabian Huch |
update to javamail-20250122;
|
changeset |
files
|
| Wed, 22 Jan 2025 22:22:37 +0000 |
paulson |
merged
|
changeset |
files
|
| Wed, 22 Jan 2025 22:22:27 +0000 |
paulson |
more tidying
|
changeset |
files
|
| Wed, 22 Jan 2025 14:43:26 +0100 |
Fabian Huch |
tuned messages;
|
changeset |
files
|
| Wed, 22 Jan 2025 11:23:35 +0100 |
Fabian Huch |
clarified: more arguments;
|
changeset |
files
|
| Wed, 22 Jan 2025 10:53:20 +0100 |
Fabian Huch |
explicit error message when Solr database does not exist;
|
changeset |
files
|
| Wed, 22 Jan 2025 10:35:17 +0100 |
Fabian Huch |
copy instead of symlink managed Find_Facts indexes: portable, and allows updating with local sessions;
|
changeset |
files
|
| Tue, 21 Jan 2025 17:28:09 +0100 |
Fabian Huch |
clarified CLI arg vs. option;
|
changeset |
files
|
| Tue, 21 Jan 2025 17:19:30 +0100 |
Fabian Huch |
clarified;
|
changeset |
files
|
| Tue, 21 Jan 2025 17:15:52 +0100 |
Fabian Huch |
clarified find_facts URL;
|
changeset |
files
|
| Tue, 21 Jan 2025 17:13:06 +0100 |
Fabian Huch |
clarified CLI options: web dir only in $FIND_FACTS_HOME_USER/web;
|
changeset |
files
|
| Tue, 21 Jan 2025 15:55:30 +0100 |
Fabian Huch |
clarified settings: $FIND_FACTS_HOME_USER instead of individual directories;
|
changeset |
files
|
| Tue, 21 Jan 2025 15:31:57 +0100 |
Fabian Huch |
clarified: Find_Facts indexes instead of Solr components;
|
changeset |
files
|
| Tue, 21 Jan 2025 14:36:47 +0100 |
Fabian Huch |
clarified: application-specific $SOLR_DATA, e.g. $FIND_FACTS_SOLR_DATA;
|
changeset |
files
|
| 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
|
| 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
|
| Thu, 16 Jan 2025 10:09:33 +0000 |
paulson |
More tidying of old proofs
|
changeset |
files
|
| Thu, 16 Jan 2025 09:26:58 +0100 |
haftmann |
dropped redundant material (left-over from 5e3dd01a9eb2)
|
changeset |
files
|
| Thu, 16 Jan 2025 09:26:57 +0100 |
haftmann |
explicit check for (experimentally determined) border value
|
changeset |
files
|
| Thu, 16 Jan 2025 09:26:56 +0100 |
haftmann |
theory to rewrite arithmetic operations to bit shifts
|
changeset |
files
|
| Wed, 15 Jan 2025 17:48:38 +0100 |
nipkow |
merge
|
changeset |
files
|
| Wed, 15 Jan 2025 16:45:12 +0100 |
nipkow |
Compact notation for Suc numerals.
|
changeset |
files
|
| Wed, 15 Jan 2025 13:55:58 +0100 |
traytel |
store the {l,g}fp-definition and the monotonicity theorem for inductive predicates (by Jan van Brügge)
|
changeset |
files
|
| Wed, 15 Jan 2025 13:54:28 +0100 |
traytel |
make the definition of BNF bounds more easily accessible (by Jan van Brügge)
|
changeset |
files
|
| Wed, 15 Jan 2025 13:53:25 +0100 |
traytel |
avoid theorem name clash (by Jan van Brügge)
|
changeset |
files
|
| Wed, 15 Jan 2025 13:53:03 +0100 |
traytel |
introduce fewer constants in copy_bnf/lift_bnf (by Jan van Brügge)
|
changeset |
files
|
| Tue, 14 Jan 2025 22:35:03 +0000 |
paulson |
Some work on an ancient theory file. And a weird failure in Float.thy
|
changeset |
files
|
| Tue, 14 Jan 2025 21:50:44 +0000 |
paulson |
simplified old proofs
|
changeset |
files
|
| Tue, 14 Jan 2025 18:46:58 +0000 |
paulson |
polished messy proofs
|
changeset |
files
|