Changes
merged
(detail / hgweb ) 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 ) 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 ) 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 ) ![[Jenkins]](/jenkins/static/109fb1e5/images/svgs/logo.svg){kind=logo}
