Changes
Some hyphens that should be en dashes
(detail / hgweb ) slightly refine WPO-definitiondetail / hgweb ) merged
(detail / hgweb ) no "open" of ML structures: it makes sources unmaintainable;
(detail / hgweb ) adapted to Isabelle/5db014c36f42;
(detail / hgweb ) adapted to Isabelle/f4cd6e3b5075;
(detail / hgweb ) adapted to Isabelle/5db014c36f42;
(detail / hgweb ) This file should have been removed in the previous commit.
(detail / hgweb ) Sync with my development repo. Main changes related to CartesianMonoidalCategory.
(detail / hgweb ) update timing;
(detail / hgweb ) eliminated pointless parallelism: approx. 1.3s as plain sequential ML;
(detail / hgweb ) tuned;
(detail / hgweb ) alternative version by Manuel Eberl, following the approach of Isabelle2022/src/HOL/Tools/sat.ML with one big hyp;
(detail / hgweb ) adapted to Isabelle/c274f52b11ff;
(detail / hgweb ) Backed out changeset a537fb4c92af
(detail / hgweb ) slightly faster thanks to Thm.shared_context from Isabelle/4f9117e6020d;
(detail / hgweb ) merged
(detail / hgweb ) moved lemma to FDS exercises
(detail / hgweb ) Fix proofs broken by previous commit.
(detail / hgweb ) Add congurence rule for bind_tm in Root_Balanced_Tree.Time_Monaddetail / hgweb ) tuned;
(detail / hgweb ) tuned;
(detail / hgweb ) eliminated aliases: prefer existing Thm.elim_implies;
(detail / hgweb ) tuned;
(detail / hgweb ) more standard use of structure Unsynchronized;
(detail / hgweb ) tuned whitespace;
(detail / hgweb ) not unused!
(detail / hgweb ) Added running time analysis
(detail / hgweb ) some remarks on division
(detail / hgweb ) clarified scope of document
(detail / hgweb ) no subsection without section
(detail / hgweb ) merged
(detail / hgweb ) Deleted library material
(detail / hgweb ) adapted to Isabelle/b43ee37926a9;
(detail / hgweb ) merged
(detail / hgweb ) adapted to Isabelle/13cee8c2ed8d;
(detail / hgweb ) Add related entry for Combinatorial_Enumeration_Algorithms.detail / hgweb ) small simplifications
(detail / hgweb ) shortened some parts of Huffman proof using Sledgehammer
(detail / hgweb ) added another simplification rule when alternatives are equal
(detail / hgweb ) added more simplification rules involving Zero
(detail / hgweb ) adapted to Isabelle/4a174bea55e2;
(detail / hgweb ) uodated map update syntax
(detail / hgweb ) Adjusted to changes in distribution.
(detail / hgweb ) more realistic timeout;
(detail / hgweb ) avoid hardwired documents;detail / hgweb ) merged
(detail / hgweb ) simplified a few proofs
(detail / hgweb ) added character sets to the extension directory of regular expressions
(detail / hgweb ) more syntax adjustments
(detail / hgweb ) more syntax update for map update syntax
(detail / hgweb ) more map update syntax updates
(detail / hgweb ) merged
(detail / hgweb ) updated to new map update syntax priorities
(detail / hgweb ) Some simplifications of proofs
(detail / hgweb ) Minor refinements
(detail / hgweb ) tiny simplifications
(detail / hgweb ) tidied another file
(detail / hgweb ) tidied a bit more
(detail / hgweb ) merged
(detail / hgweb ) More tidying
(detail / hgweb ) completed the addtion of Rec in the Extension directory
(detail / hgweb ) added another regular expression for Record
(detail / hgweb ) More tidying of the Ordinal entry
(detail / hgweb ) A massive tidying
(detail / hgweb ) Tiny bit more tidying
(detail / hgweb ) more robust: allow optional arguments in isabelle.Progress.echo;
(detail / hgweb ) More tidying
(detail / hgweb ) merged
(detail / hgweb ) Suppression of duplicate syntax for abs_summable_on, etc.
(detail / hgweb ) No more sorted_take, sorted_drop
(detail / hgweb ) Update entries MDP-Rewards and MDP-Algorithms
(detail / hgweb ) Migration of material from Jordan_Hoelder to HOL-Algebra
(detail / hgweb ) merged
(detail / hgweb ) Tidied up some messy proofs
(detail / hgweb ) Adjustments for the new infix status of has_sum
(detail / hgweb ) A tiny spelling correction
(detail / hgweb ) merged
(detail / hgweb ) A little more migration
(detail / hgweb ) Backed out changeset fa59c080cb3b
(detail / hgweb ) Backed out changeset 811f0b8d4f58
(detail / hgweb ) tuned metis call to avoid obscure feature
(detail / hgweb ) merged
(detail / hgweb ) Migration of material to the repository and necessary modifications
(detail / hgweb ) more map_of adaptions
(detail / hgweb ) adapted to new List.map_of
(detail / hgweb ) update Real_Time_Deque
(detail / hgweb ) Removal of a stray sledgehammer command
(detail / hgweb ) explicit range types in abstractions
(detail / hgweb ) somehow more clear terminology
(detail / hgweb ) merged
(detail / hgweb ) Some tidying and moving some material to the distribution
(detail / hgweb ) Deleted use of Euclidean_Division
(detail / hgweb ) Repaired session name
(detail / hgweb ) "Repaired boundary behaviour of mod+- for even modulus, Added locale module_spec for possible instantiation of Dilithium"
(detail / hgweb ) Update names to match thesis.
(detail / hgweb ) proper components base, following "isabelle components -I": downloaded components should be shared for all Isabelle versions;
(detail / hgweb ) proper symbolic handle on component resources (see Isabelle/3eb3de867786);
(detail / hgweb ) more realistic timeout, based on CPU time;
(detail / hgweb ) adapted to Isabelle/9a60c1759543;
(detail / hgweb ) more realistic timeout, based on CPU time;
(detail / hgweb ) fixed looping proofs
(detail / hgweb ) dropped reference to dead clone
(detail / hgweb ) removed dead clone
(detail / hgweb ) modernized
(detail / hgweb ) Modernized.
(detail / hgweb ) More instances.
(detail / hgweb ) Tuned whitespace.
(detail / hgweb ) Updated references.
(detail / hgweb ) More correct references.
(detail / hgweb ) Removed a bit of unnecessary material
(detail / hgweb ) merged
(detail / hgweb ) Shortened several messy proofs
(detail / hgweb ) Fix name clash in Frequency_Moments.
(detail / hgweb ) Fixed a name clash
(detail / hgweb ) Moving more material to the distribution
(detail / hgweb ) Moving some material to the main repository
(detail / hgweb ) adapted to db93f67a;
(detail / hgweb ) merged
(detail / hgweb ) generalized theory name: euclidean division denotes one particular division definition on integers
(detail / hgweb ) more efficient specification
(detail / hgweb ) merge from afp-2022
(detail / hgweb ) metadata for Suppes' theorem + sitegen
(detail / hgweb ) new entry: Suppes' Theorem
(detail / hgweb ) new entry HoareForDivergence
(detail / hgweb ) tuned css;
(detail / hgweb ) metadat for StrictOmegaCategories
(detail / hgweb ) new entry StrictOmegaCategories
(detail / hgweb ) tuned css;
(detail / hgweb ) cleanup accidental unused document files;
(detail / hgweb ) check ROOTs: add warning-only checks;
(detail / hgweb ) tuned;
(detail / hgweb ) add ROOT checks for document presence and unused files;
(detail / hgweb ) afp-submit visual improvements;
(detail / hgweb ) update bibtex example;
(detail / hgweb ) new doi
(detail / hgweb ) sitegen for AOT
(detail / hgweb ) merged
(detail / hgweb ) New entry AOT
(detail / hgweb ) New entry: Propositional_Logic_Class
(detail / hgweb ) sitegen for Cook_Levin
(detail / hgweb ) New entry Cook_Levin
(detail / hgweb ) Sorry — extra files for Boolos_Curious_Inference_Automated
(detail / hgweb ) Metadata for /Users/lp15/.isabelle/Isabelle2022/browser_info/AFP/Boolos_Curious_Inference_Automated
(detail / hgweb ) New entry Boolos_Curious_Inference_Automated
(detail / hgweb ) New entry: Synthetic_Completeness
(detail / hgweb ) New entry: Quantifier_Elimination_Hybrid
(detail / hgweb ) New entry Birkhoff_Finite_Distributive_Lattices
(detail / hgweb ) sitegen for Kneser_Cauchy_Davenport
(detail / hgweb ) metadata for Kneser_Cauchy_Davenport
(detail / hgweb ) new entry: Kneser_Cauchy_Davenport
(detail / hgweb ) sitegen for Turan
(detail / hgweb ) added metadata for Turans graph theorem
(detail / hgweb ) new entry: Turans Graph Theorem
(detail / hgweb ) new entry Multitape_To_Singletape_TM
(detail / hgweb ) removed static pages from rss feed;
(detail / hgweb ) Minor rerating of the abstract of Sauer_Shelah_Lemma
(detail / hgweb ) sitegen for /Users/lp15/.isabelle/Isabelle2022/browser_info/AFP/Sauer_Shelah_Lemma
(detail / hgweb ) New entry Sauer_Shelah_Lemma
(detail / hgweb ) sitegen for the aforementioned changes
(detail / hgweb ) adjustments to the abstract, requested by the author
(detail / hgweb ) CHERI-C_Memory_Model patch & metadata
(detail / hgweb ) New submission CHERI-C_Memory_Model
(detail / hgweb ) updated docs;
(detail / hgweb ) improve page layout slightly;
(detail / hgweb ) fixed broken abstract for PAPP_Impossibility
(detail / hgweb ) remove dead code
(detail / hgweb ) metadata and sitegen for PAPP_Impossibility
(detail / hgweb ) new entry PAPP_Impossibility
(detail / hgweb ) remove old .sitegen-ignore and mention AFP chapter in submission guidelines;
(detail / hgweb ) afp_check_roots: proper error message printing;
(detail / hgweb ) metadata and sitegen for Balog_Szemeredi_Gowers
(detail / hgweb ) new entry: Balog_Szemeredi_Gowers
(detail / hgweb ) tuned check names;
(detail / hgweb ) make check roots tool less dependent on AFP structure;
(detail / hgweb ) tuned;
(detail / hgweb ) web for Combinatorial_Enumeration_Algorithms
(detail / hgweb ) sitegen for Combinatorial_Enumeration_Algorithms
(detail / hgweb ) New entry Combinatorial_Enumeration_Algorithms
(detail / hgweb ) fix duplicate affiliations from author and notify;
(detail / hgweb ) add metadata check tool to sitegen;
(detail / hgweb ) update check tools: add formatting checks, new cmd options;
(detail / hgweb ) check for entries instead of session due to session nesting allowed in entries;
(detail / hgweb ) added unused thy check;
(detail / hgweb ) clarified check roots tool;
(detail / hgweb ) afp-submit: tuned logging;
(detail / hgweb ) afp-submit: encode new notify addresses properly;
(detail / hgweb ) afp-submit: correct build status on empty file;
(detail / hgweb ) afp-submit: remove padding on select;
(detail / hgweb ) re-format metadata;
(detail / hgweb ) afp-submit: update on correct status change;
(detail / hgweb ) afp-submit: clarified date format, tuned logging;
(detail / hgweb ) switch fonts to www prefixed isa-afp.org domain;
(detail / hgweb ) switch to www prefixed isa-afp.org domain;
(detail / hgweb ) clarified afp-submit error handling;
(detail / hgweb ) clarified afp-submit creation and message;
(detail / hgweb ) list submission system website;
(detail / hgweb ) afp-submit: clarified api urls;
(detail / hgweb ) Removal of more unused material
(detail / hgweb ) Small simplifications. Removed a needless assumption.
(detail / hgweb ) isabelle update -u cite;
(detail / hgweb ) more accurate root.bib, based on original \bibitem entries in root.tex 1a42ddd5dbbc;
(detail / hgweb ) Fixed the bib issues and supplied a root.bib based on the one in Types_Tableaus_and_Goedels_God (by the same author)
(detail / hgweb ) merged
(detail / hgweb ) Added the missing .bib file
(detail / hgweb ) proper bib context for formal citations, although there is no document;
(detail / hgweb ) back to unchecked \cite: entry lacks .bib file;
(detail / hgweb ) back to unchecked \cite: entry lacks .bib file;
(detail / hgweb ) back to unchecked \cite: there is entry lacks .bib file;
(detail / hgweb ) proper citation;
(detail / hgweb ) merged
(detail / hgweb ) added lemmas image_grounding_of_cls_grounding_of_cls and grounding_of_clss_grounding_of_clss[simp]
(detail / hgweb ) merged
(detail / hgweb ) isabelle update -u cite;
(detail / hgweb ) merged
(detail / hgweb ) consistent casing in \cite
(detail / hgweb ) ETTS: updated bibliography and citations
(detail / hgweb ) merged
(detail / hgweb ) more correct and complete citations;
(detail / hgweb ) unchecked \cite for unidentifiable citation;
(detail / hgweb ) proper @{cite} syntax;
(detail / hgweb ) isabelle update -u cite;
(detail / hgweb ) Updating Risk Free Lending Entrydetail / hgweb ) added bibliography to ROOT;
(detail / hgweb ) CTR and ETTS: several amendments (fact names, printing, presentation)
(detail / hgweb ) Removed a reference to the (redundant) wf_restr
(detail / hgweb ) added bibliographies to ROOTs;
(detail / hgweb ) Changes for generalised lemmas
(detail / hgweb ) Changes for generalised lemmas
(detail / hgweb ) Generalised Lemmas
(detail / hgweb ) merged
(detail / hgweb ) adapted to Isabelle/c9e091867206
(detail / hgweb ) tuned;
(detail / hgweb ) tuned signature, following Isabelle/947510ce4e36;
(detail / hgweb ) adapted to Isabelle/25900fbea7ad;detail / hgweb ) adapted to Isabelle/b61ad889dffa
(detail / hgweb ) removed Restricted_Predicates.transp_on following the introduction of equivalent Relation.transp_on in HOL
(detail / hgweb ) merged
(detail / hgweb ) adapted to Isabelle/d33fc5228aae
(detail / hgweb ) fixed proof following Isabelle/66cae055ac7b
(detail / hgweb ) merge
(detail / hgweb ) adapted to Isabelle/c48fe2be847f
(detail / hgweb ) enable -no-pie for CakeML
(detail / hgweb ) fixed proofs and removed duplicates following Isabelle/e65a50f6c2de
(detail / hgweb ) tuned proofs to use asymI, asymD, asympI, and asympD
(detail / hgweb ) Fix failing continuous integration
(detail / hgweb ) fixed proof following Isabelle/8fff4e4d81cb
(detail / hgweb ) removed Restricted_Predicates.antisymp_on following the introduction of equivalent Relation.antisymp_on in HOL
(detail / hgweb ) added lemma imgu_range_vars_subset
(detail / hgweb ) Update headers and metadata.
(detail / hgweb ) Fix ROOT again
(detail / hgweb ) Fix ROOT
(detail / hgweb ) Use transfinite induction to prove Lindenbaum's lemma, removing the countable assumption.
(detail / hgweb ) Fixed proofs following Isabelle/a7d2a7a737b8
(detail / hgweb ) added lemmas mem_range_varsI and imgu_subst_domain_subset
(detail / hgweb ) weakened the definition of redundant_inference
(detail / hgweb ) removed Restricted_Predicates.irreflp_on following the introduction of equivalent Relation.irreflp_on in HOL
(detail / hgweb ) fixed Containers following introduction of irrefl_on
(detail / hgweb ) added lemmas ex_unify_if_unifiers_not_empty, ex_mgu_if_unifiers_not_empty, and imgu_range_vars_of_equations_vars_subset
(detail / hgweb ) name change
(detail / hgweb ) AFP and DBLP
(detail / hgweb ) merged
(detail / hgweb ) added lemmas subst_range_rename_subst_domain_subset and range_vars_rename_subst_domain_subset
(detail / hgweb ) added lemma subst_domain_rename_subst_domain_subset
(detail / hgweb ) added lemma image_the_Var_image_subst_renaming_eq
(detail / hgweb ) Added acknowledgements
(detail / hgweb ) Added code export to ROOT
(detail / hgweb ) Removed out of place code
(detail / hgweb ) tuned lemma subst_domain_restrict_subst_domain
(detail / hgweb ) added lemmas rename_subst_domain_range_Var_lhs[simp] and rename_subst_domain_range_Var_rhs[simp]
(detail / hgweb ) added attribute [simp] to lemma rename_subst_domain_Var_rhs
(detail / hgweb ) added lemmas inj_on_Var[simp] and rename_subst_domain_Var_lhs[simp]
(detail / hgweb ) merged
(detail / hgweb ) removed Restricted_Predicates.reflp_on following the introduction of equivalent Relation.reflp_on in HOL
(detail / hgweb ) removed Restricted_Predicates.total_on following the introduction of equivalent Relation.totalp_on in HOL
(detail / hgweb ) added lemmas grounding_of_subst_cls_renaming_ident[simp] and grounding_of_subst_clss_renaming_ident[simp]
(detail / hgweb ) added lemmas is_ground_cls_add_mset[simp], grounding_of_subst_cls_subset, and grounding_of_subst_clss_subset
(detail / hgweb ) Streamlined a proof
(detail / hgweb ) added lemmas
(detail / hgweb ) moved lemma around
(detail / hgweb ) redefined mgu as a definition
(detail / hgweb ) tuned naming
(detail / hgweb ) fixed proof
(detail / hgweb ) added definition restrict_subst_domain and associated lemmas
(detail / hgweb ) tuned (sub)subsection
(detail / hgweb ) added lemma member_image_the_Var_image_subst
(detail / hgweb ) added lemmas unify_subst_domain_range_vars_disjoint
(detail / hgweb ) added lemma unify_range_vars
(detail / hgweb ) added lemma unify_subst_domain
(detail / hgweb ) added definition rename_subst_domain_range and related lemmas
(detail / hgweb ) merged
(detail / hgweb ) added lemmas vars_term_subst_apply_term and vars_term_subst_apply_term_subset
(detail / hgweb ) Fixed the ROOT file, so that the theory of cardinals is loaded
(detail / hgweb ) added lemma ex_mgu_if_subst_apply_term_eq_subst_apply_term
(detail / hgweb ) added lemmas unify_append_prefix_same, unify_Cons_same, unify_same, and mgu_same
(detail / hgweb ) added lemma decompose_same_Fun[simp]
(detail / hgweb ) added lemma zip_option_same[simp]
(detail / hgweb ) added definition rename_subst_domain and lemma renaming_cancels_rename_subst_domain
(detail / hgweb ) removed simp annotation from subst_apply_term_eq_subst_apply_term_if_mgu
(detail / hgweb ) used rho for renamming
(detail / hgweb ) tuned assumptions
(detail / hgweb ) added lemma subst_apply_term_eq_subst_apply_term_if_mgu
(detail / hgweb ) added lemmas inv_renaming_sound and ex_inverse_of_renaming
(detail / hgweb ) added lemma subst_apply_term_ident
(detail / hgweb ) added lemmas subst_range_Var and range_vars_Var and moved stuff around
(detail / hgweb ) added lemma subst_apply_term_subst_apply_term_eq_subst_apply_term_lhs and tuned naming
(detail / hgweb ) tuned naming
(detail / hgweb ) added lemma mgu_range_vars
(detail / hgweb ) added lemma subst_compose_apply_eq_apply_lhs_if
(detail / hgweb ) added lemmas is_Var_mgu_if_not_in_equations, ball_is_Var_mgu, and inj_on_mgu
(detail / hgweb ) RealTimeDeque: replace `reverseN` with `take_rev
(detail / hgweb ) replaced Open_Induction.Restricted_Predicates.total_on by equivalent HOL.Relation.totap_on
(detail / hgweb ) merge from afp-2022
(detail / hgweb ) add missing thy files in Sturm_Tarski + repair
(detail / hgweb ) afp-submit: style page, improve elements;
(detail / hgweb ) afp-submit: added repository updates;
(detail / hgweb ) afp-submit: added download and faster file handling;
(detail / hgweb ) add submission pages to web ui;
(detail / hgweb ) afp-submit: add submission and build status with adapter to existing system;
(detail / hgweb ) add user-facing exception handling to web app;
(detail / hgweb ) clarified submission handling;
(detail / hgweb ) afp-submit: added submission read-only and list views;
(detail / hgweb ) add afp-submit web app;
(detail / hgweb ) add web app facilities;
(detail / hgweb ) RealTimeDeque: Separate implementation and auxiliary functions
(detail / hgweb ) Backed out changeset 3a67df508397detail / hgweb ) adapted to new simproc finite
(detail / hgweb ) clarified signature, following Isabelle/f362975e8ba1;
(detail / hgweb ) more direct Proof_Context.init_global;
(detail / hgweb ) proper naming conventions for Isabelle/ML;
(detail / hgweb ) Updated citation
(detail / hgweb ) merge from afp-2022
(detail / hgweb ) Isabelle2022: new release download links
(detail / hgweb ) Added tag Isabelle2022 for changeset 548e384c0445
(detail / hgweb ) import 2022 release dates
(detail / hgweb ) entry names not restricted to alpha-numeric
(detail / hgweb ) add 2021-1 all releases;
(detail / hgweb ) clarified docs
(detail / hgweb ) replace old get-releases tool (now isabelle afp_release -I);
(detail / hgweb ) add option for parallel session builds
(detail / hgweb ) set Isabelle2022 release date
(detail / hgweb ) set release version to 2022
(detail / hgweb ) merge from afp-2021-1
(detail / hgweb ) Removal of some old junk
(detail / hgweb ) Deleted unused material
(detail / hgweb ) nothing
(detail / hgweb ) Instantiation of the order solver for ⊑ and ⊏ (no real effect though)
(detail / hgweb ) proof simplifications
(detail / hgweb ) merged
(detail / hgweb ) Simplified the proofs a bit
(detail / hgweb ) merged
(detail / hgweb ) replaced fmember.rep_eq by fmember_iff_member_fset
(detail / hgweb ) merge from afp-2021-1
(detail / hgweb ) only make parent dir;
(detail / hgweb ) accept all dois;
(detail / hgweb ) metadata toml: tuned error messages;
(detail / hgweb ) clarified sub topics;
(detail / hgweb ) adapted to Isabelle/457f1cba78fb
(detail / hgweb ) merged
(detail / hgweb ) added lemmas generalizes_lit_refl[simp] and generalizes_lit_trans;detail / hgweb ) extracted proof cases from lifting_lemma to distinct lemmas
(detail / hgweb ) tuned proof due to new simp rules
(detail / hgweb ) corresponding lemma was removed from distribution
(detail / hgweb ) regen site
(detail / hgweb ) updates to BenOr_Kozen_Reif by Katherine Kosaian
(detail / hgweb ) fix author entry; regen website
(detail / hgweb ) add change history revision
(detail / hgweb ) Added scene spaces, improvements to prisms, and improvements to the alphabet command.
(detail / hgweb ) merge from afp-2021-1
(detail / hgweb ) new entry Query_Optimization
(detail / hgweb ) remove temp file
(detail / hgweb ) Complex_Bounded_Operators: Various changes:detail / hgweb ) slightly less abusive proof pattern
(detail / hgweb ) Many changes to entry `Complex_Bounded_Operators`:detail / hgweb ) tuned proofs
(detail / hgweb ) merge from afp-2021-1
(detail / hgweb ) new entry Undirected_Graph_Theory
(detail / hgweb ) typo
(detail / hgweb ) typo
(detail / hgweb ) New entry: Maximum_Segment_Sum
(detail / hgweb ) regenerate site;
(detail / hgweb ) added topic for data management systems;
(detail / hgweb ) added missing file
(detail / hgweb ) New entry Safe_Range_RC
(detail / hgweb ) adjust Stalnaker_Logic to changes in Epistemic_Logic;
(detail / hgweb ) adjusted to distribution
(detail / hgweb ) remove duplicate code;
(detail / hgweb ) restructure afp ci builds (see Isabelle/3c4e373922ca)
(detail / hgweb ) Cosmetic changes.
(detail / hgweb ) merge from afp-2021-1
(detail / hgweb ) regenerate site;
(detail / hgweb ) afp site: minor stylistic improvements;
(detail / hgweb ) web entry for Stalnaker_Logic
(detail / hgweb ) new entry: Stalnaker Logic
(detail / hgweb ) clarified options, following f2094906e491;
(detail / hgweb ) Comments on theories brought from ZF-Constructible. Shortening fm names
(detail / hgweb ) adjusted to distribution
(detail / hgweb ) Remove fontenc from root.tex to make Ł show in PDF.
(detail / hgweb ) Update ROOT...
(detail / hgweb ) Appendix with another axiom system as a variant of the proof.
(detail / hgweb ) adapt to Isabelle@769a7cd5a16a
(detail / hgweb ) merge from afp-2021-1
(detail / hgweb ) adjust Lar's contact info as requested
(detail / hgweb ) sitegen for Padic_Field
(detail / hgweb ) new entry: Padic_Field
(detail / hgweb ) sitegen for Risk_Free_Lending
(detail / hgweb ) new entry: Risk_Free_Lending
(detail / hgweb ) new entry Implicational_Logic
(detail / hgweb ) New entry Separation_Logic_Unbounded
(detail / hgweb ) added web files
(detail / hgweb ) added web files
(detail / hgweb ) New entry SCC_Bloemen_Sequential
(detail / hgweb ) A few more disambiguations, related to locales in CartesianCategory.
(detail / hgweb ) Merged
(detail / hgweb ) Further disambiguation of facts to address clashes involving ConcreteCategory as a sublocale.
(detail / hgweb ) streamlined division on polynomials
(detail / hgweb ) Complex_Bounded_Operators: Fixed errors in document generation
(detail / hgweb ) Complex_Bounded_Operators: Added numerous new lemmas.
(detail / hgweb ) Merged
(detail / hgweb ) Disambiguate sufficiently many facts in locales so as to permit a top-level interpretation of ZFC_set_cat.
(detail / hgweb ) Fix a typo.
(detail / hgweb ) Neater links
(detail / hgweb ) Relational_Disjoint_Set_Forests: variant abstraction
(detail / hgweb ) merged
(detail / hgweb ) support for ISABELLE_MLTON_OPTIONS, following Isabelle/d27ed188e0c4;
(detail / hgweb ) Renaming synthesized formulas
(detail / hgweb ) prefer (smt (verit)), which is potentially more stable under heavy load;
(detail / hgweb ) Add additional results.
(detail / hgweb ) Formatting.
(detail / hgweb ) Add papers to abstracts.
(detail / hgweb ) merged
(detail / hgweb ) Purely cosmetic
(detail / hgweb ) merged
(detail / hgweb ) Deleted one redundant step
(detail / hgweb ) merged
(detail / hgweb ) Merge
(detail / hgweb ) Tidied (a lot)
(detail / hgweb ) added missing congruence rule
(detail / hgweb ) streamlined
(detail / hgweb ) tuned proofs (manually or with sledgehammer): avoid "smt" due to spurious failures under heavy load;
(detail / hgweb ) tuned whitespace;
(detail / hgweb ) merged
(detail / hgweb ) some slight polishing in the UTM entry
(detail / hgweb ) added congruence rule for forallM of Error-Monad
(detail / hgweb ) updated to devel
(detail / hgweb ) merged
(detail / hgweb ) tuned proofs (manually or with sledgehammer): avoid "smt" due to spurious failures under heavy load;
(detail / hgweb ) removed obsolete workaround (see Isabelle/91ee232b4211);
(detail / hgweb ) Eliminated the temporary material that was already migrated to the Isabelle libraries
(detail / hgweb ) merge from afp-2021-1
(detail / hgweb ) regenerate site;
(detail / hgweb ) tuned;
(detail / hgweb ) merged
(detail / hgweb ) New entry CRYSTALS-Kyber
(detail / hgweb ) regenerate site;
(detail / hgweb ) added missing history in metadata;
(detail / hgweb ) retrieve missing change history in metadata migration tool;
(detail / hgweb ) backout b2ae7c2c3ea51af8f43b76cdcb5d499c5085e726
(detail / hgweb ) new email address for Maksym
(detail / hgweb ) metadata and sitegen for Khovansikii_Theorem
(detail / hgweb ) new entry: Khovanski-Theorem
(detail / hgweb ) fixed metadata for Hales_Jewett
(detail / hgweb ) sitegen for Number_Theoretic_Transform
(detail / hgweb ) new entry Number_Theoretic_Transform
(detail / hgweb ) new entry Hales Jewett
(detail / hgweb ) adapt to only check ROOT for directories in thys (aftermath of Isabelle/a9bbf075f4319e920a22a1c0a5b763b6575f2089);
(detail / hgweb ) updated entry for Universal Turing Machines
(detail / hgweb ) merged
(detail / hgweb ) adapted to antimono
(detail / hgweb ) merged
(detail / hgweb ) adapted to new mono and strict_mono
(detail / hgweb ) updated to Isabelle/5ea588440b06
(detail / hgweb ) Updated citations
(detail / hgweb ) Updated citations
(detail / hgweb ) tuned signature;
(detail / hgweb ) merged
(detail / hgweb ) Substantial additions by Franz Regensburger to the Universal_Turing_Machine entry
(detail / hgweb ) tuned timeouts, based on test runs with threads=1;
(detail / hgweb ) replaced slow smt call by blast
(detail / hgweb ) avoid hardwired document;
(detail / hgweb ) merged
(detail / hgweb ) cosmetic
(detail / hgweb ) replace smt_oracle by proper veriT reconstruction
(detail / hgweb ) merged
(detail / hgweb ) tweaks
(detail / hgweb ) make all sessions of chapter "AFP" belong to group "AFP";
(detail / hgweb ) chapter_definition for presentation;
(detail / hgweb ) Undo an unrelated change that somehow crept into the previous commit.
(detail / hgweb ) Remove lots of unnecessary explicit quantifiers in lemma statements, now that I've discovered "arbitrary:".
(detail / hgweb ) Revised locale structure and notation. Proposed modularization for ZF-Constructible's M_eclose
(detail / hgweb ) tuning
(detail / hgweb ) updated entries: Combinatorics_Words, Combinatorics_Words_Lyndon, and Combinatorics_Words_Graph_Lemma
(detail / hgweb ) avoid fact name clash
(detail / hgweb ) adjusted to distribution
(detail / hgweb ) repaired proof
(detail / hgweb ) Complex_Bounded_Operators: Fixed document generation
(detail / hgweb ) Merged changes.
(detail / hgweb ) Registers: Fixed parse error.
(detail / hgweb ) Misc updates to Complex_Bounded_Operators:detail / hgweb ) Reintroduce type signatures.
(detail / hgweb ) Switch to simultaneous substitutions.
(detail / hgweb ) merge from afp-2021-1
(detail / hgweb ) new entry: Nano_JSON
(detail / hgweb ) sitegen for Commuting_Hermitian
(detail / hgweb ) new entry: Commuting_Hermitian
(detail / hgweb ) Sitegen for Involutions2Squares (WITH WRONG EMAIL ADDRESS)
(detail / hgweb ) new entry Involutions2Squares
(detail / hgweb ) fix typo
(detail / hgweb ) new entry Solidity
(detail / hgweb ) tuned title
(detail / hgweb ) more typos
(detail / hgweb ) regenerate because of typos
(detail / hgweb ) New entry
(detail / hgweb ) topics no longer exist
(detail / hgweb ) new topics
(detail / hgweb ) New entry FSM_Tests
(detail / hgweb ) merged
(detail / hgweb ) Isabelle/b6589c8ccadd officially supports README.thy;
(detail / hgweb ) streamlined
(detail / hgweb ) tuned proofs
(detail / hgweb ) discontinued obsolete README.html: superseded by abstract provided by AFP;
(detail / hgweb ) streamlined primitive definitions for integer division
(detail / hgweb ) tuned code equations for Xml-parsing
(detail / hgweb ) refactored algebraic number theories, generalized Cauchy Root Bounds lemma (so that real and complex numbers work)
(detail / hgweb ) Revision of locale structure
(detail / hgweb ) Purely markup
(detail / hgweb ) Fix ImpSplit thy for document generation
(detail / hgweb ) Add B+Tree formalisation to the BTree entry
(detail / hgweb ) Correcting thm antiquotations. Turning code comments into text
(detail / hgweb ) Update metadata and root.tex to mention the addition of ZFC_SetCat in early 2022.
(detail / hgweb ) Sync with my development repo: Category3: add various rules for limits. RTS: strengthen definition of transformation.
(detail / hgweb ) adapted to NLists.thy
(detail / hgweb ) merged
(detail / hgweb ) use Library/NList.thy now
(detail / hgweb ) Further streamlining of quick-and-dirty evaluation.
(detail / hgweb ) An attempt for an integrated solution for quick-and-dirty evaluation.
(detail / hgweb ) Further reduction of locale assumptions
(detail / hgweb ) merged
(detail / hgweb ) more complete theorem_commands;
(detail / hgweb ) clarified signature, following Isabelle/b6d74c90b588;
(detail / hgweb ) Update metadata for Frequency_Moments.
(detail / hgweb ) merged
(detail / hgweb ) Update Schutz_Spacetimedetail / hgweb ) more accurate name
(detail / hgweb ) more politically correct
(detail / hgweb ) two new lemmas
(detail / hgweb ) added two lemmas to relational chains
(detail / hgweb ) changed confusing assumption name
(detail / hgweb ) avoid the surprise that n-m is 0 even if n<m.
(detail / hgweb ) tuned
(detail / hgweb ) simplified invar
(detail / hgweb ) merged
(detail / hgweb ) simplified
(detail / hgweb ) update metadata;
(detail / hgweb ) merged
(detail / hgweb ) tuned
(detail / hgweb ) removed a spurious locale parameter -- the same issue probably arises in the pen-and-paper Waldmann et al.
(detail / hgweb ) removed needless assumption
(detail / hgweb ) Named intermediate results combinable wands
(detail / hgweb ) Named intermediate results Package logic
(detail / hgweb ) added lemma about lazy list chains
(detail / hgweb ) typo
(detail / hgweb ) Refining three sessions.detail / hgweb ) Tuned.
(detail / hgweb ) merged
(detail / hgweb ) addd DOIs and other metadata links
(detail / hgweb ) some slight polishing of the definitions
(detail / hgweb ) added links
(detail / hgweb ) added metadata links
(detail / hgweb ) added link
(detail / hgweb ) added Wiki link
(detail / hgweb ) added DOIs
(detail / hgweb ) added DIs
(detail / hgweb ) added DOIs
(detail / hgweb ) Added DOIs
(detail / hgweb ) added DOIs
(detail / hgweb ) added DOIs
(detail / hgweb ) merged
(detail / hgweb ) added DOIs
(detail / hgweb ) XZ compression for Safe_Distance examples (safes 160 MB!)
(detail / hgweb ) tuned DOIs
(detail / hgweb ) added DOIs
(detail / hgweb ) added DOIs
(detail / hgweb ) added DOIs
(detail / hgweb ) added pubs
(detail / hgweb ) merge from afp-2021-1
(detail / hgweb ) improve DOI resolving: offline cache and better timeouts;
(detail / hgweb ) added pubs
(detail / hgweb ) added DOIs
(detail / hgweb ) merge from afp-2021-1
(detail / hgweb ) resolve DOIs in sitegen to formatted citations;
(detail / hgweb ) removed links from related references;
(detail / hgweb ) regenerate site;
(detail / hgweb ) Remove duplication between Universal_Hash_Families (UHF) and Finite_Fields (FF).detail / hgweb ) Update metadata for WOOT_Strong_Eventual_Consistency.detail / hgweb ) added DOI
(detail / hgweb ) added DOI
(detail / hgweb ) merged
(detail / hgweb ) added orcid
(detail / hgweb ) added orcid
(detail / hgweb ) added lemma
(detail / hgweb ) ORCID for Manuel Eberl
(detail / hgweb ) merge from afp-2021-1
(detail / hgweb ) updated help page;
(detail / hgweb ) clarified doc;
(detail / hgweb ) name change for Kądziołka
(detail / hgweb ) updated docs on metadata;
(detail / hgweb ) adjusted topics and added subject classifications;
(detail / hgweb ) name change for Kądziołka
(detail / hgweb ) moved lemma to distribution
(detail / hgweb ) merge from afp-2021-1
(detail / hgweb ) added more metadata fields: related references for entries, orcids for authors, and acm/ams subject classification for topics;
(detail / hgweb ) tuned topics
(detail / hgweb ) adjusted topics
(detail / hgweb ) proper license link;
(detail / hgweb ) tuned;
(detail / hgweb ) merge from afp-2021-1
(detail / hgweb ) regenerate site;
(detail / hgweb ) sitegen: integrate change history and note properly;
(detail / hgweb ) tuned;
(detail / hgweb ) clarified homepage urls;
(detail / hgweb ) remove metadata migration tool;
(detail / hgweb ) toml parser improvements: comments are now treated as whitespace.
(detail / hgweb ) clarified metadata loading and added more metadata checks;
(detail / hgweb ) regenerate site;
(detail / hgweb ) improve releases view and map correctly to Isabelle version;
(detail / hgweb ) add missing releases again;
(detail / hgweb ) merged
(detail / hgweb ) sitegen for Weighted_Arithmetic_Geometric_Mean
(detail / hgweb ) new entry Weighted_Arithmetic_Geometric_Mean
(detail / hgweb ) missing file
(detail / hgweb ) New entry IMP_Compiler_Reuse
(detail / hgweb ) Just variable renamings
(detail / hgweb ) merged
(detail / hgweb ) Simplified and shortened some proofs
(detail / hgweb ) moved lemmas to distribution
(detail / hgweb ) merged
(detail / hgweb ) tweaked
(detail / hgweb ) merged
(detail / hgweb ) a bit of tidying
(detail / hgweb ) cleanup with global-interpretations and code equations in Simplex_Incremental
(detail / hgweb ) changed incremental simplex interface: check now always returns a new state, even in unsat-case
(detail / hgweb ) merge from afp-2021-1
(detail / hgweb ) Improvements.
(detail / hgweb ) regenerate site;
(detail / hgweb ) sitegen: tuned statistics;
(detail / hgweb ) tuned;
(detail / hgweb ) sitegen for Boolos_Curious_Inference
(detail / hgweb ) new entry: Boolos_Curious_Inference
(detail / hgweb ) website: proper bibtex entries;
(detail / hgweb ) tuned
(detail / hgweb ) removed more material now residing in distribution
(detail / hgweb ) separated non-computable instance of bit comprehension from computable one
(detail / hgweb ) Small changes.
(detail / hgweb ) Undo accidental changes.
(detail / hgweb ) Tuned.
(detail / hgweb ) tuned -- follow clone in $ISABELLE_HOME/src/HOL/Imperative_HOL/Heap_Monad.thy;
(detail / hgweb ) minor performance tuning: avoid redundant BigInt construction;
(detail / hgweb ) prefer self-made Array.T, to avoid problems with ArraySeq in Scala 3;
(detail / hgweb ) more robust Array.T for Scala 2.13 and 3.x, following Isabelle/ca450d902198;
(detail / hgweb ) Move code lemmas for symbolic computation of bit operations on int to distribution.
(detail / hgweb ) renamings
(detail / hgweb ) Relational_Disjoint_Set_Forests: improved abstractions
(detail / hgweb ) Simplified a proof using Cauchy–Schwarz
(detail / hgweb ) removed precondition in det_four_block_mat
(detail / hgweb ) merge
(detail / hgweb ) removed assumption in det_bound_hadamard_tight, moved some basic lemmas on matrices, added a conditional version of det(four_block_mat ...) = ...
(detail / hgweb ) merge from afp-2021-1
(detail / hgweb ) updated doc;
(detail / hgweb ) regenerate site;
(detail / hgweb ) obfuscate email addresses in metadata and generated site;
(detail / hgweb ) renamed det_bound_gram to det_bound_hadamard, showed that bound is tight (using unproven fact about determinants of block-matrices)
(detail / hgweb ) added lemma for special case of small integer solutions (no mixed integer), where then everything is of type int
(detail / hgweb ) document change in metadata
(detail / hgweb ) generalized fixed bounds on determinants to predicate; added an improved determinate bounddetail / hgweb ) Code generated in the same directory
(detail / hgweb ) Removed ML code from AFP entry
(detail / hgweb ) adapted to scala-3.1.2;
(detail / hgweb ) merge from afp-2021-1
(detail / hgweb ) tuned;
(detail / hgweb ) tooling: added utility to check for metadata consistency;
(detail / hgweb ) regenerate website;
(detail / hgweb ) site: generate multi-line json for smaller merges;
(detail / hgweb ) toml module: proper parsing of quotes in multiline strings;
(detail / hgweb ) added further sitegen generated websites
(detail / hgweb ) added metadata for Real_Time_Deque's, sitegen
(detail / hgweb ) new entry: Real-Time Double-Ended Queue
(detail / hgweb ) merged
(detail / hgweb ) replaced IMGU by min_IMGU
(detail / hgweb ) replaced MGU by IMGU
(detail / hgweb ) exposed that inverse of renaming only maps variables to variables
(detail / hgweb ) added the r{n..} regular expression to the extensions directory in the Posix-Lexing entry, added two small lemmas to the Regular-Set theory
(detail / hgweb ) merge from afp-2021-1
(detail / hgweb ) regenerate website
(detail / hgweb ) do not ignore admin/site
(detail / hgweb ) remove afp python component build tool;
(detail / hgweb ) afp tooling: improve keyword extraction;
(detail / hgweb ) website: small improvements;
(detail / hgweb ) tuned efficiency of XML parser
(detail / hgweb ) tuned
(detail / hgweb ) updated the abstract in root.tex
(detail / hgweb ) added the r{..n} regular expression to the extensions directory
(detail / hgweb ) merged
(detail / hgweb ) tuned BNF bound
(detail / hgweb ) strict bounds for BNFs (by Jan van Brügge)
(detail / hgweb ) merge from afp-2021-1 (replaying devel commit)
(detail / hgweb ) replaced python RAKE component with Isabelle/Scala Rake component;
(detail / hgweb ) remove scala tools from publish;
(detail / hgweb ) replaced python RAKE component with Isabelle/Scala Rake component;
(detail / hgweb ) merged
(detail / hgweb ) avoid hardwired pdf;
(detail / hgweb ) adapted to Isabelle/986506233812;
(detail / hgweb ) merged
(detail / hgweb ) added an implementation of pseudo remainder sequences for calculating Tarski queries
(detail / hgweb ) merged
(detail / hgweb ) updated to Isabelle/3c544d64c218
(detail / hgweb ) merge from afp-2021-1
(detail / hgweb ) tuned error messages;
(detail / hgweb ) mention error location when metadata loading fails;
(detail / hgweb ) merged
(detail / hgweb ) even more IsaNet;
(detail / hgweb ) afp metadata/releases: change format to re-add releases swallowed by key-set, remove extra releases;
(detail / hgweb ) more IsaNet
(detail / hgweb ) New entry IsaNet
(detail / hgweb ) adapted to Isabelle/39df30349778;
(detail / hgweb ) added extension that deals with the n-times regular expression in Posix-Lexing
(detail / hgweb ) Avoid calculations where not necessary.
(detail / hgweb ) used long version of definition to avoid conflict when introducing HOL.monotone_on
(detail / hgweb ) merge from afp-2021-1 (metadata consolidation)
(detail / hgweb ) sitegen
(detail / hgweb ) unified home pages
(detail / hgweb ) re-introduce accidentally reverted changes
(detail / hgweb ) ignore dev site output
(detail / hgweb ) consolidate metadata (email and homepages)
(detail / hgweb ) merge from afp-2021-1
(detail / hgweb ) load mail configuration lazily (initialized later from properties);
(detail / hgweb ) tuned home pages
(detail / hgweb ) merge from afp-2021-1
(detail / hgweb ) tuned;
(detail / hgweb ) proper topics loading;
(detail / hgweb ) merge from afp-2021-1 (new website)
(detail / hgweb ) new website
(detail / hgweb ) admin: remove old sitegen lib files
(detail / hgweb ) update metadata to new sitegen
(detail / hgweb ) merge website-redesign graft
(detail / hgweb ) updated afp sitegen doc;
(detail / hgweb ) replaced python afp stats with Isabelle/Scala tool;
(detail / hgweb ) updated afp metadata doc (now as markdown);
(detail / hgweb ) afp components: removed unnecessary platforms;
(detail / hgweb ) afp sitegen: switch to new version;
(detail / hgweb ) add sitegen ignore option;
(detail / hgweb ) improvements for toml module: proper boolean values;
(detail / hgweb ) add components as proper afp deps;
(detail / hgweb ) tuned;
(detail / hgweb ) switched to standalone cross-platform afp python component;
(detail / hgweb ) tuned;
(detail / hgweb ) afp python build: use tgz for better cross-plattform compatability;
(detail / hgweb ) replaced ci_profiles by statically compiled afp_build tool (Scala 3 preparations);
(detail / hgweb ) afp structure: added accessors;
(detail / hgweb ) hugo site: minor changes;
(detail / hgweb ) hugo-site: improve various aspects;
(detail / hgweb ) add new authors to migration;
(detail / hgweb ) clarified formatting, for the sake of scala3;
(detail / hgweb ) hugo site: better scrolling;
(detail / hgweb ) hugo site: updated devel info;
(detail / hgweb ) hugo site: updated content;
(detail / hgweb ) hugo site: proper ordering;
(detail / hgweb ) hugo site: restricted generated affiliations;detail / hgweb ) hugo site: proper theory view link scrolling;
(detail / hgweb ) hugo site: tuned affiliation keys;
(detail / hgweb ) hugo site: proper topic-only topics page;
(detail / hgweb ) hugo site: relativize paths;
(detail / hgweb ) hugo site: list sessions separately;
(detail / hgweb ) hugo site: tuned;
(detail / hgweb ) hugo site: tuned;
(detail / hgweb ) hugo site: merge gen and build tool;
(detail / hgweb ) hugo site: added doc headers;
(detail / hgweb ) hugo site: tuned;
(detail / hgweb ) afp metadata: index keys for emails and urls;detail / hgweb ) hugo site: improve theory view;
(detail / hgweb ) hugo site: cleaned up;
(detail / hgweb ) hugo site: added devel version;
(detail / hgweb ) hugo site: updated search and content;
(detail / hgweb ) hugo site: added theory view styling for different device sizes;detail / hgweb ) Updated metadata in migration and theory view;
(detail / hgweb ) hugo site: updated site templates;
(detail / hgweb ) metadata migration: updated authors;
(detail / hgweb ) hugo: added mobile view;
(detail / hgweb ) hugo: copy to proper path;
(detail / hgweb ) added theory navbar;
(detail / hgweb ) tuned formatting;
(detail / hgweb ) added loader;
(detail / hgweb ) tuned;
(detail / hgweb ) tuned: more canonical Isabelle code style;
(detail / hgweb ) proper loading of foundational hrefs;
(detail / hgweb ) fix dependencies;
(detail / hgweb ) added devel flag;
(detail / hgweb ) updated about page;
(detail / hgweb ) moved extraction of related entries to hugo;
(detail / hgweb ) improved keyword extraction;
(detail / hgweb ) added keywords to site generated entry data;
(detail / hgweb ) use tmp file for python script instead of command;
(detail / hgweb ) added js-side theory loading to afp site;
(detail / hgweb ) integrated metadata changes into site;detail / hgweb ) added missing keyword data;
(detail / hgweb ) removed html dir from sitegen (now set inside hugo);
(detail / hgweb ) tuned sitegen: moved dependencies generation to scala
(detail / hgweb ) changed generated author format;
(detail / hgweb ) tuned;
(detail / hgweb ) tuned;
(detail / hgweb ) tuned hugo: static files more explicit;
(detail / hgweb ) tuned;
(detail / hgweb ) proper authors/affiliations gen for hugo taxonomy;
(detail / hgweb ) clarified hugo data;
(detail / hgweb ) added missing name mapping to migration;
(detail / hgweb ) proper output path;
(detail / hgweb ) added missing topics;
(detail / hgweb ) clarified hugo build signature;detail / hgweb ) added more steps to afp site generation tool;
(detail / hgweb ) tuned;detail / hgweb ) added hugo project by Carlin MacKenzie;
(detail / hgweb ) added sitegen scripts by Carlin MacKenzie (slightly tweaked);
(detail / hgweb ) added afp hugo module;
(detail / hgweb ) clarified afp_dependencies: proper typed output;detail / hgweb ) Added afp structure module;
(detail / hgweb ) Added python wrapper;
(detail / hgweb ) clarified metadata;
(detail / hgweb ) tuned;
(detail / hgweb ) added afp hugo component;
(detail / hgweb ) added afp python component with required packages;
(detail / hgweb ) feat(afp/tools): added initial site build tool
(detail / hgweb ) tuned(afp/tools): metadata sorted
(detail / hgweb ) tuned(afp/tools): tuned parser/unparser
(detail / hgweb ) feat(afp/tools): more metadata and toml conversion;
(detail / hgweb ) feat(afp/tools): added TOML lexer and parser;
(detail / hgweb ) tuned(afp/tools): module jar locations;
(detail / hgweb ) fix(afp/tools): added missing metadata, improved toml structure
(detail / hgweb ) fix(afp/tools): removed TOML formatting heuristics for simplicity;
(detail / hgweb ) feat(afp/tools): added TOML module;
(detail / hgweb ) feat(afp/tools): added metadata migration tool;
(detail / hgweb ) feat(afp/tools): migrated scala tool_bodys to proper tools;
(detail / hgweb ) Avoid explicit operation when not necessary.
(detail / hgweb ) adjust for isabelle@5bba3516ddb5
(detail / hgweb ) merge from afp-2021-1
(detail / hgweb ) Added a missing acknowledgement
(detail / hgweb ) metadata for Finite_Fields (and missing <> for two previous entries)
(detail / hgweb ) new entry: Finite_Fields
(detail / hgweb ) sitegen for DPRM_Theorem
(detail / hgweb ) DPRM_Theorem: finally cleaned up and impressive!
(detail / hgweb ) New entry [Rewrite_Properties_Reduction]
(detail / hgweb ) Fixed broken LaTeX in the abstract
(detail / hgweb ) sitegen for Combinable_Wands
(detail / hgweb ) New entry Combinable_Wands
(detail / hgweb ) corrected metadata (separate authors by "," not by "and")
(detail / hgweb ) sitegen and metadata for Pluennecke_Ruzsa_Inequality
(detail / hgweb ) new entry: Pluennecke Ruzsa Inequality
(detail / hgweb ) Tuning the abstract to remove some of the display mathematics
(detail / hgweb ) sitegen for Package_logic
(detail / hgweb ) new entry Package_logic
(detail / hgweb ) Removal of all email addresses, at authors' request
(detail / hgweb ) renamed some variables
(detail / hgweb ) proper \open\close markup
(detail / hgweb ) Updated the Posix-Lexer entry including a small change in Regular-Set
(detail / hgweb ) Trimmed down dependencies.
(detail / hgweb ) Merge equivalent instance declarations for functions in Lp.Functional_Spaces and HOL-Library.Function_Algebras.detail / hgweb ) Remove duplicate lemma and fix typos in Frequency_Moments.
(detail / hgweb ) same variant as for imperative algorithm to prove n^2 complexity
(detail / hgweb ) tuned
(detail / hgweb ) Shortened and simplified a proof
(detail / hgweb ) more realistic timeout;
(detail / hgweb ) tuned whitespace;
(detail / hgweb ) more realistic timeout;detail / hgweb ) avoid hard-wired document;
(detail / hgweb ) removed usages of HOL.no_atp as its content and order is not guaranteed
(detail / hgweb ) cleaning
(detail / hgweb ) no separate code-equations required for a lift_definition by using (code_dt) instead
(detail / hgweb ) The last few occurrences of integrable_cong
(detail / hgweb ) Tidying/removal of obsolete material
(detail / hgweb ) Fixed a use of Bochner_Integration.integrable_cong
(detail / hgweb ) fixes for compatibility with renamed / new lemmas
(detail / hgweb ) Tiny simplifications
(detail / hgweb ) A tiny bit of reorganisation
(detail / hgweb ) the last "simp/auto" problems
(detail / hgweb ) corrected all "bysimp"
(detail / hgweb ) Automated merge with bundle:/var/folders/9z/l1x9y3bd16x9_70pdp4703jr0000gp/T/SourceTreeTemp.3gPj1U
(detail / hgweb ) Tidied auto/simp with null arguments
(detail / hgweb ) merged
(detail / hgweb ) comleted single loop refinement
(detail / hgweb ) minor adjustments
(detail / hgweb ) metadata
(detail / hgweb ) minor amendments
(detail / hgweb ) creation and preservation of limits; a variety of auxiliary results and amendments
(detail / hgweb ) patched a broken proof
(detail / hgweb ) merged
(detail / hgweb ) single lopp variant refined to lists.
(detail / hgweb ) adjust for isabelle@7095df141819
(detail / hgweb ) merge from afp-2021-1
(detail / hgweb ) typo fix
(detail / hgweb ) sitegen for Digit_Expansions
(detail / hgweb ) New entry Digit_Expansions
(detail / hgweb ) finally!!!! Sitegen for Sophomore's Dream
(detail / hgweb ) merged
(detail / hgweb ) Minor corrections to metadata (no "and" between authors' names)
(detail / hgweb ) Updating the version of Jinja2, as suggested by Manuel
(detail / hgweb ) merged
(detail / hgweb ) updated metadata
(detail / hgweb ) new entry Sophomores_Dream
(detail / hgweb ) updated name and email address of Rose Bohrer
(detail / hgweb ) sitegen for Clique_and_Monotone_Circuits
(detail / hgweb ) new entry Clique_and_Monotone_Circuits
(detail / hgweb ) metadata and sitegen for Fisher's inequality
(detail / hgweb ) new entry: Fisher's Inequality
(detail / hgweb ) New entry Multiset_Ordering_NPC
(detail / hgweb ) sitegen for Frequence_Moments
(detail / hgweb ) new entry: Frequence_Moments
(detail / hgweb ) metadata and sitegen for Prefix_Free_Code_Combinators
(detail / hgweb ) new entry: Prefix_Free_Code_Combinators
(detail / hgweb ) regen website (some orders are different in python3)
(detail / hgweb ) switch sitegen to python3
(detail / hgweb ) sitegen for new entry
(detail / hgweb ) new entry: FOL_Seq_Calc3
(detail / hgweb ) New entry: Dedekind_Real
(detail / hgweb ) New entry Ackermann_not_PR, from distribution
(detail / hgweb ) Cotangent_PFD_Formula sitegen
(detail / hgweb ) new entry Cotangent_PFD_Formula
(detail / hgweb ) website for Independence_CH
(detail / hgweb ) new entry Independence_CH
(detail / hgweb ) New entry ResiduatedTransitionSystem
(detail / hgweb ) Transitive_Models webpage
(detail / hgweb ) new entry Transitive_Models
(detail / hgweb ) updated name and email address of Rose Bohrer
(detail / hgweb ) Removal of unnecessary material
(detail / hgweb ) perfectly pointless streamlining
(detail / hgweb ) More general definition of gcard
(detail / hgweb ) refined one-loop version further
(detail / hgweb ) tidied up a few proofs
(detail / hgweb ) A bit of beautification
(detail / hgweb ) Yet more tidying and streamlining of graph lemmas
(detail / hgweb ) merged
(detail / hgweb ) A few trivial changes
(detail / hgweb ) Tweaks concerning the versions of Zhao's evolving lecture notes
(detail / hgweb ) Trying to simplify a bit more
(detail / hgweb ) More simplification of proofs. Removal of numeric references to Zhao.
(detail / hgweb ) tidying and simplification
(detail / hgweb ) merged
(detail / hgweb ) More purely cosmetic changes
(detail / hgweb ) moved from AFP to distribution
(detail / hgweb ) tuned syntax
(detail / hgweb ) simplified some proofs and deleted quite a bit of redundant material
(detail / hgweb ) Shorter proofs and leaner notation.
(detail / hgweb ) Minor updates supplied by the author, mostly connected with a reference to a work by Hilbert, now deleted.
(detail / hgweb ) Add a construction, using ZFC_in_HOL, of the category of small sets and functions.
(detail / hgweb ) Resolve a "Duplicate constant declaration" issue that occurs with "isabelle build -o export_theory".
(detail / hgweb ) avoid side effects on working copy while runnign sessions (generated code is unused)
(detail / hgweb ) clarified formatting, for the sake of scala3;
(detail / hgweb ) Deleted a few redundant lines
(detail / hgweb ) Trying to beautify this, but it's still ugly
(detail / hgweb ) And a bit more tidying
(detail / hgweb ) more renaming and tidying
(detail / hgweb ) Alphabetic substitutions
(detail / hgweb ) Eliminated another finiteness assumption
(detail / hgweb ) Removal of some needless finiteness assumptions
(detail / hgweb ) Removed a small amount of redundant material from both Szemerédi and Roth
(detail / hgweb ) merged
(detail / hgweb ) tidied up a few proofs
(detail / hgweb ) A slightly nicer proof
(detail / hgweb ) merged
(detail / hgweb ) tidied and generalised some proofs using small_eqpoll
(detail / hgweb ) merged
(detail / hgweb ) tidied some proofs
(detail / hgweb ) Improved handling splitting theorems in the alphabet command
(detail / hgweb ) Fixed wrong sign handling in fmul-add
(detail / hgweb ) more count_list lemmas
(detail / hgweb ) more count_list
(detail / hgweb ) merged
(detail / hgweb ) moved some count_list lemmas
(detail / hgweb ) synchronize with https://gitlab.lisn.upsaclay.fr/burkhart.wolff/Isabelle_C/-/tree/5f38d029bfcabac8ba3b4ceea747f07772d1390d
(detail / hgweb ) synchronize with https://gitlab.lisn.upsaclay.fr/burkhart.wolff/Isabelle_C/-/tree/5f38d029bfcabac8ba3b4ceea747f07772d1390d
(detail / hgweb ) synchronize with https://gitlab.lisn.upsaclay.fr/burkhart.wolff/Isabelle_C/-/tree/5f38d029bfcabac8ba3b4ceea747f07772d1390d
(detail / hgweb ) synchronize with https://gitlab.lisn.upsaclay.fr/burkhart.wolff/Isabelle_C/-/tree/5f38d029bfcabac8ba3b4ceea747f07772d1390d
(detail / hgweb ) continue 98838b260ed4
(detail / hgweb ) continue ee01bce2ecca
(detail / hgweb ) cancel some part of 11d4567f1b99
(detail / hgweb ) cancel some part of 98838b260ed4
(detail / hgweb ) cancel some part of ada85c62541d
(detail / hgweb ) synchronize with https://gitlab.lisn.upsaclay.fr/burkhart.wolff/Isabelle_C/-/tree/5f38d029bfcabac8ba3b4ceea747f07772d1390d
(detail / hgweb ) split locale in two
(detail / hgweb ) Stronger strong completeness result and variant that uses variables as Henkin witnesses.
(detail / hgweb ) Stronger strong completeness result and variant that uses variables as Henkin witnesses.
(detail / hgweb ) added some alternative proofs in Smith_Normal_Form entry
(detail / hgweb ) The last tranche of material to be moved to the complex analysis libraries
(detail / hgweb ) Removal of material that has since been added to ZFC_in_HOL.General_Cardinals
(detail / hgweb ) Deleted nearly 200 lines of unused material
(detail / hgweb ) A new theorem
(detail / hgweb ) Clarified code module names.
(detail / hgweb ) removed ancient numeral representation
(detail / hgweb ) restore state of VYDRA_MDL to b8c3f69745a4
(detail / hgweb ) merge from afp-2021-1
(detail / hgweb ) metadata for Universal_Hash_Families
(detail / hgweb ) new entry Universal_Hash_Families
(detail / hgweb ) New entry Wetzel's Problem
(detail / hgweb ) metadata for Eval_FO
(detail / hgweb ) new entry Eval_FO
(detail / hgweb ) metadata for VYDRA_MDL
(detail / hgweb ) new entry VYDRA_MDL
(detail / hgweb ) Backed out changeset c9f94b0ae10e
(detail / hgweb ) Backed out changeset b8c3f69745a4
(detail / hgweb ) metadata update for VYDRA_MDL
(detail / hgweb ) New entry: VYDRA_MDL
(detail / hgweb ) fixed failing proofs
(detail / hgweb ) New definition of the Aleph operator so that it's defined for all arguments, not just ordinals
(detail / hgweb ) ALEXANDRIA acknowledgements
(detail / hgweb ) merged
(detail / hgweb ) New set theory lemmas about cardinality (mainly)
(detail / hgweb ) Another attempt for a consolidated terminology.
(detail / hgweb ) Avoid overaggresive splitting.
(detail / hgweb ) more lemmas for distribution
(detail / hgweb ) Avoid overaggresive simplification.
(detail / hgweb ) some new lemmas
(detail / hgweb ) merged
(detail / hgweb ) More material
(detail / hgweb ) added idempotent most general unifier
(detail / hgweb ) used same parameter order for locales substitution and substitution
(detail / hgweb ) patched for new/simplified lemmas
(detail / hgweb ) Better notation.
(detail / hgweb ) merge from afp-2021-1
(detail / hgweb ) avoid conflict with index.html in generated html
(detail / hgweb ) New entry: FO_Theory_Rewriting
(detail / hgweb ) Improve consistency of type-variables in WOOT_Strong_Eventual_Consistency.detail / hgweb ) Improve proofs for Interpolation_Polynomials_HOL_Algebra.detail / hgweb ) Correct date.
(detail / hgweb ) deleted a lemma that's in the devel library
(detail / hgweb ) Cleanup and new results.
(detail / hgweb ) moved theorems into Matrix.thy
(detail / hgweb ) merge of AFP 2021-1
(detail / hgweb ) New AFP entry: Equivalence_Relation_Enumeration
(detail / hgweb ) new entry: LP_Duality
(detail / hgweb ) cosmetic tweaks
(detail / hgweb ) sitegen and metadata for Young's inequality
(detail / hgweb ) new entry: Young's inequality
(detail / hgweb ) metadata for Quasi_Borel_Spaces, sitegen
(detail / hgweb ) new entry: Quasi_Borel_Spaces
(detail / hgweb ) sitegen for FOL_Seq_Calc2
(detail / hgweb ) new entry FOL_Seq_Calc2
(detail / hgweb ) tweak: corollary that the ln also yields irrational numbers
(detail / hgweb ) New entry: Interpolation_Polynomials_HOL_Algebra
(detail / hgweb ) Finally remembered to run sitegen
(detail / hgweb ) Fixed the meta data in the abstract as well
(detail / hgweb ) Eliminated the references to SOS (which is no longer used) and changed to the document style to "article".
(detail / hgweb ) typo
(detail / hgweb ) typo
(detail / hgweb ) New entry Irrationals_From_THEBOOK
(detail / hgweb ) new entry Median_Method
(detail / hgweb ) Actuarial Mathematics website
(detail / hgweb ) New entry Actuarial_Mathematics
(detail / hgweb ) Strong soundness.
(detail / hgweb ) Strong soundness.
(detail / hgweb ) Fix LaTeX issue.
(detail / hgweb ) Qualification required(?)
(detail / hgweb ) merged
(detail / hgweb ) more variants of the algorithm
(detail / hgweb ) Added funding acknowledgments.detail / hgweb ) Strong completeness for PAL systems.
(detail / hgweb ) Cleanup.
(detail / hgweb ) Fewer parentheses around turnstile + remove unused lemmas.
(detail / hgweb ) Simplify proof of truth lemma.
(detail / hgweb ) Notation for `imply` and fewer parenthesis around turnstiles.
(detail / hgweb ) Abstract results to shorten proofs.
(detail / hgweb ) Better notation.
(detail / hgweb ) merged
(detail / hgweb ) tuned whitespace;
(detail / hgweb ) more symbols;
(detail / hgweb ) profer bundle lattice_syntax;
(detail / hgweb ) prefer existing lattice_syntax and no_lattice_syntax, with proper 'no_notation' as intended;
(detail / hgweb ) Add soundness and completeness for the PAL versions of systems K, T, KB, K4, S4 and S5.
(detail / hgweb ) avoid hardwired document output;
(detail / hgweb ) merged
(detail / hgweb ) deleting the overloading of div and mod, with its attendant ambiguities
(detail / hgweb ) replaced Erdős by Erd\H{o}s (fixed problem in LaTeX document generation)
(detail / hgweb ) Removal of a lemma (now in the libraries) and a few tweaks
(detail / hgweb ) Tuning.
(detail / hgweb ) merged
(detail / hgweb ) tweaks
(detail / hgweb ) merged
(detail / hgweb ) Fixed an inadequate description
(detail / hgweb ) tuned
(detail / hgweb ) mv to distribution
(detail / hgweb ) by now in distribution
(detail / hgweb ) merge from afp-2021-1
(detail / hgweb ) fixed abstract
(detail / hgweb ) tuned
(detail / hgweb ) website and metadata for Hyperdual
(detail / hgweb ) new entry: Hyperdual
(detail / hgweb ) sorted ROOTS
(detail / hgweb ) tuned
(detail / hgweb ) New entry Knights_Tour
(detail / hgweb ) more thoroughly replace Michael Foster's e-mail address
(detail / hgweb ) metadata and sitegen for Gale_Shapley
(detail / hgweb ) new entry Gale_Shapley
(detail / hgweb ) update Michael Forster's email address
(detail / hgweb ) metadata and sitegen for Roth_Arithmetic_Progressions
(detail / hgweb ) new entry Roth_Arithmetic_Progressions
(detail / hgweb ) typo
(detail / hgweb ) merged
(detail / hgweb ) New entry Regular_Tree_Relations
(detail / hgweb ) We DON'T want an output directory
(detail / hgweb ) MDP-Algorithms website
(detail / hgweb ) new entry MDP-Algorithms
(detail / hgweb ) typo
(detail / hgweb ) new entry MDP-Rewards
(detail / hgweb ) fixed typo
(detail / hgweb ) CS: possibility to disable backtracking; CZH: auxiliary results; ETTS: minor amendments
(detail / hgweb ) used wfP_imp_asymp from HOL
(detail / hgweb ) simplified proof some more
(detail / hgweb ) simplified proof
(detail / hgweb ) Extended protocol model to support composition of more than two protocols withoutdetail / hgweb ) Tweaked some failing proofs
(detail / hgweb ) adapted to new Sledgehammer.run_sledgehammer return type
(detail / hgweb ) Strengthened a lemma
(detail / hgweb ) updated the definition of scheme
(detail / hgweb ) merge from afp-2021-1
(detail / hgweb ) add change history
(detail / hgweb ) updated 2021-1 release dates -> web
(detail / hgweb ) merge from afp-2021-1
(detail / hgweb ) ignore generated files
(detail / hgweb ) add 2021-1 release dates
(detail / hgweb ) set devel version again
(detail / hgweb ) Added tag Isabelle2021-1 for changeset 11f8b03a88ad
(detail / hgweb ) adjust usage version
(detail / hgweb ) set release version
(detail / hgweb ) update release dates
(detail / hgweb ) merge from afp-2021-1
(detail / hgweb ) The version without integer indexes
(detail / hgweb ) The version without integer indexes
(detail / hgweb ) merge from afp-2021-1
(detail / hgweb ) merge from afp-2021
(detail / hgweb ) new entry Foundation_of_geometry
(detail / hgweb ) merge from afp-2021-1
(detail / hgweb ) Modified all design locale parameters to be nats instead of ints. Fixed proofs as required.
(detail / hgweb ) adjust for Isabelle2021-1-RC5
(detail / hgweb ) merge from afp-2021
(detail / hgweb ) new entry Simplicial_complexes_and_boolean_functions
(detail / hgweb ) Modified all design locale parameters to be nats instead of ints. Fixed proofs as required.
(detail / hgweb ) merge from afp-2021-1
(detail / hgweb ) adjust to Isabelle2021-1-RC5
(detail / hgweb ) merge from afp-2021
(detail / hgweb ) metadata and sitegen for Hahn_Jordan_Decomposition
(detail / hgweb ) added Mathematics/Measure theory
(detail / hgweb ) new entry: Hahn_Jordan_Decomposition
(detail / hgweb ) New entry: Van_Emde_Boas_Trees
(detail / hgweb ) New entry: Van_Emde_Boas_Trees
(detail / hgweb ) metadata and sitegen for SimplifiedOntologicalArgument
(detail / hgweb ) new entry: SimplifiedOntologicalArgument
(detail / hgweb ) Tuned: use a star in witness.
(detail / hgweb ) Rename H to S in maximal_exactly_one.
(detail / hgweb ) Get rid of the sat abbreviation.
(detail / hgweb ) Add missing spaces in semantics_tm.
(detail / hgweb ) No space in front of object-logic forall.
(detail / hgweb ) Non-conflicting name for boolean denotation.
(detail / hgweb ) Simpler Hintikka definition.
(detail / hgweb ) Add syntactic abbreviation for constants.
(detail / hgweb ) Add papers to metadata.
(detail / hgweb ) In the definition of regular pair, switched from strict to non-strict
(detail / hgweb ) A slightly stronger lemma allowing slightly simpler proofs
(detail / hgweb ) merged
(detail / hgweb ) generalized standard formula redundancy out of standard redundancy
(detail / hgweb ) merged
(detail / hgweb ) discontinued Parse.text;
(detail / hgweb ) discontinued old-style {* verbatim *} tokens;
(detail / hgweb ) weakened locale assumptions: wfP implies asymp
(detail / hgweb ) Add papers to metadata.
(detail / hgweb ) refactored Standard_Redundancy_Criterion to not use ordering type classes
(detail / hgweb ) isabelle update_cartouches;
(detail / hgweb ) removed obsolete "extend" operation;
(detail / hgweb ) more symbolic latex_output via XML (using YXML within text);detail / hgweb ) prefer symbolic Latex.environment (typeset in Isabelle/Scala);
(detail / hgweb ) tuned signature;
(detail / hgweb ) feat(Auto2_HOL) fix setup such that auto2 can be used by other object logics and multiple times
(detail / hgweb ) Tuned: use a star in witness.
(detail / hgweb ) merge from afp-2021-1
(detail / hgweb ) adjust for new tags in Isabelle2021-1-RC4
(detail / hgweb ) fix dangerous context management
(detail / hgweb ) In the definition of regular pair, switched from strict to non-strict
(detail / hgweb ) Rename H to S in maximal_exactly_one.
(detail / hgweb ) Get rid of the sat abbreviation.
(detail / hgweb ) Add missing spaces in semantics_tm.
(detail / hgweb ) No space in front of object-logic forall.
(detail / hgweb ) Non-conflicting name for boolean denotation.
(detail / hgweb ) Simpler Hintikka definition.
(detail / hgweb ) Add syntactic abbreviation for constants.
(detail / hgweb ) fixed lemma following Isabelle/c256bba593f3
(detail / hgweb ) ![[Jenkins]](/jenkins/static/f7776f3e/images/svgs/logo.svg){kind=logo}
