Changes
fix dangerous context management
(detail / hgweb ) A slightly stronger lemma allowing slightly simpler proofs
(detail / hgweb ) Complex_Bounded_Operators: Removed some lemmas from Extra_General that are now in Isabelle itself
(detail / hgweb ) Elimination of all z3 calls
(detail / hgweb ) Word_Lib sync from l4v; tweak word_eqI
(detail / hgweb ) generalise word_eqI method; make sure it is exercised
(detail / hgweb ) test_bit_size not longer needed; avoid potential nontermination
(detail / hgweb ) Word_Lib tweaks for slightly more backwards compatibility
(detail / hgweb ) use bit_simps in word_eqI method
(detail / hgweb ) adapted to new version of Infinite_Sum in isabelle-dev
(detail / hgweb ) avoid hardwired document output;
(detail / hgweb ) CTR and ETTS: integration with SpecCheck: minor amendments
(detail / hgweb ) Complex_Bounded_Operators: Replaced use of HOL-Analysis.Infinite_Set_Sum by HOL-Analysis.Infinite_Sum
(detail / hgweb ) Banach_Steinhaus: Removed unused theory dependency Infinite_Set_Sum
(detail / hgweb ) merge
(detail / hgweb ) merge
(detail / hgweb ) Merge Isabelle_C: New C11_Ast_Lib Interface, improved API's, improved doc.
(detail / hgweb ) documentation fine-tuning.
(detail / hgweb ) Added section on C11_Ast_Lib in chapter II.
(detail / hgweb ) Example section restored and Documentation adapted.
(detail / hgweb ) Stramge intermediate configuration: Example section zerschossen.
(detail / hgweb ) Port to Isabelle2021-1 RC 2.
(detail / hgweb ) Improved documentation.
(detail / hgweb ) Examples for iterator - applications: queries, and translations into term.
(detail / hgweb ) Rearranging standard root store; better documentation in C_Command.
(detail / hgweb ) Rearranging the ML _programming Example Section C1.
(detail / hgweb ) reorg 1
(detail / hgweb ) ...
(detail / hgweb ) Improved Standard Interface to C11: Better signatures, a CEnv signature, C11 Std Ast Store (in C2.thy)
(detail / hgweb ) Restructuring of Interfaces; more show cases.
(detail / hgweb ) Updated meta-data for Optics
(detail / hgweb ) Additional scene laws
(detail / hgweb ) Branch merge
(detail / hgweb ) Improved support for code generation, fixed a few bugs, and added a tactic to aid proof goal presentation of lens variables.
(detail / hgweb ) feat(SpecCheck/Show) add parentheses for option SOME case
(detail / hgweb ) merged
(detail / hgweb ) weakened ordering requirements
(detail / hgweb ) used well-founded pre-order in standard redundancy criterions
(detail / hgweb ) derived refutational completeness from finitary and non-finitary standard redundancy criterion
(detail / hgweb ) merge
(detail / hgweb ) deleted incomplete methods for polynomial factorization or root computation in Algebraic-Numbers, sincedetail / hgweb ) factor_complex_poly delivers distinct list
(detail / hgweb ) merged
(detail / hgweb ) Removal of material that's going to be in Isabelle2021-1
(detail / hgweb ) merge
(detail / hgweb ) refactoring (moving theories and lemmas around)
(detail / hgweb ) sync from l4v
(detail / hgweb ) adjusted Factor_Algebraic_Polynomial to Isabelle/devel (and Isabelle 2021-1, RC3)
(detail / hgweb ) merge of afp-2021
(detail / hgweb ) new entry PAL
(detail / hgweb ) new entry Factor_Algebraic_Polynomial
(detail / hgweb ) merge from afp-2021
(detail / hgweb ) document `publish -`
(detail / hgweb ) changed affiliation of eberl (this time properly)
(detail / hgweb ) changed affiliation of Eberl
(detail / hgweb ) sitegen for Real_Power
(detail / hgweb ) new entry Real_Power
(detail / hgweb ) New entry Szemeredi_Regularity
(detail / hgweb ) tuned proofs -- avoid z3;
(detail / hgweb ) CTR and ETTS: integration with SpecCheck
(detail / hgweb ) used antiquotation to fix LaTeX failure
(detail / hgweb ) adapted to devel
(detail / hgweb ) updated to devel
(detail / hgweb ) merged
(detail / hgweb ) tuned proof for devel
(detail / hgweb ) clarified quotes vs. apostrophes vs. primes;
(detail / hgweb ) more accurate use of LaTeX ndash;
(detail / hgweb ) prefer portable LaTeX mdash;
(detail / hgweb ) tuned whitespace --- removed suspicious Unicode;
(detail / hgweb ) proper Unix linefeeds;
(detail / hgweb ) changed affiliation of eberl (this time properly)
(detail / hgweb ) changed affiliation of eberl
(detail / hgweb ) added author to Saturation_Framework_Extensions
(detail / hgweb ) derived calculus_with_standard_redundancy lemmas from calculus_with_finitary_standard_redundancy
(detail / hgweb ) added locale calculus_with_finitary_standard_redundancy
(detail / hgweb ) Registers:detail / hgweb ) feat(SpecCheck) add better unit tests facilities, examples and exceptions property
(detail / hgweb ) discontinued somewhat pointless and slightly outdated document_preprocessor (after consultation with the author);
(detail / hgweb ) Correctness_Algebras: increase nitpick timeout
(detail / hgweb ) CZH: dagger monoidal categories
(detail / hgweb ) update it Isabelle/925b46043b84
(detail / hgweb ) merge from afp-2021
(detail / hgweb ) sitegen for Registers
(detail / hgweb ) new entry Registers
(detail / hgweb ) Correctness_Algebras: increase session timeout
(detail / hgweb ) tuned signature, according to Isabelle/df12779c3ce8;
(detail / hgweb ) feat(SpecCheck) add possibility to make builds fail on failure and extend README
(detail / hgweb ) added missing funding information
(detail / hgweb ) restored theory structure for simple genericity.
(detail / hgweb ) Backed out changeset af549be0a8cd
(detail / hgweb ) restored different entrance points a before Isabelle2021
(detail / hgweb ) proper parentheses (amending 354560d7143a);
(detail / hgweb ) Adjusted to prospective release Isabelle2021-2.
(detail / hgweb ) Correctness_Algebras: uncomment counterexamples
(detail / hgweb ) clarified identity of theory data: avoid accidental pointer_eq, use equality on unique serial instead;
(detail / hgweb ) clarified identity of theory data: pointer_eq is not well-defined (and fails on ARM64), use equality on unique serial instead;
(detail / hgweb ) merge from afp-2021
(detail / hgweb ) remove unused functions
(detail / hgweb ) silence sitegen warning
(detail / hgweb ) new entry X86_Semantics
(detail / hgweb ) adjust to isabelle@549019b4a808
(detail / hgweb ) merge from afp-2021
(detail / hgweb ) metadata for Belief_Revision
(detail / hgweb ) new entry Belief_Revision
(detail / hgweb ) New entry Correctness_Algebras
(detail / hgweb ) prefer "sat_solver = MiniSat", to make examples work uniformly on all platforms;
(detail / hgweb ) updated metadata for Count_Complex_Roots
(detail / hgweb ) corrected the timeout for CZH_Universal_Constructions
(detail / hgweb ) CZH: further results about comma categories and Kan extensions, a variety of other minor amendments
(detail / hgweb ) more generic bit/word lemmas for distribution
(detail / hgweb ) Fixing a name clash between two different "restrict" operators
(detail / hgweb ) Merged
(detail / hgweb ) solved the roots-on-the-border problem
(detail / hgweb ) split Count_Complex_Roots
(detail / hgweb ) more realistic timeout;
(detail / hgweb ) clarified signature, according to Isabelle/ccf599864beb;
(detail / hgweb ) back to dedicated separate shift operations for infix syntax;detail / hgweb ) ![[Jenkins]](/jenkins/static/109fb1e5/images/svgs/logo.svg){kind=logo}
