6 months ago wenzelm 2019-04-02 tuned;
6 months ago paulson 2019-04-02 The order of a group now follows the HOL Light definition, which is more general
6 months ago paulson 2019-04-02 merged
6 months ago paulson 2019-04-02 merged
6 months ago paulson 2019-04-02 some new group theory results: integer group, trivial group, etc.
6 months ago wenzelm 2019-04-02 more convenient export;
6 months ago wenzelm 2019-04-02 misc tuning for release;
6 months ago wenzelm 2019-04-02 more material for release;
6 months ago wenzelm 2019-04-02 misc tuning for release;
6 months ago wenzelm 2019-04-01 'code_reflect' only supports new-style 'file_prefix'; avoid fragile file "$ISABELLE_TMP/rat.ML";
6 months ago wenzelm 2019-04-01 tuned signature -- more exports;
6 months ago wenzelm 2019-04-01 tuned signature;
6 months ago paulson 2019-04-01 A few results in Algebra, and bits for Analysis
6 months ago haftmann 2019-03-30 experimental commands for proof sketching and exploration
6 months ago haftmann 2019-03-30 irrelevant
6 months ago wenzelm 2019-03-30 more PIDE markup and hyperlinks;
6 months ago wenzelm 2019-03-30 clarified signature: more explicit type Path.binding; tuned;
6 months ago wenzelm 2019-03-30 more LaTeX symbols;
6 months ago wenzelm 2019-03-29 tuned signature -- more operations;
6 months ago wenzelm 2019-03-29 tuned signature;
6 months ago wenzelm 2019-03-29 clarified 'file_prefix';
6 months ago wenzelm 2019-03-29 clarified style: allow to search PDF for keywords containing "_";
6 months ago wenzelm 2019-03-28 "export_code ... file_prefix ..." is the preferred way to produce output within the logical file-system within the theory context, as well as session exports; "export_code ... file" is legacy, the empty name form has been discontinued; updated examples;
6 months ago wenzelm 2019-03-28 removed junk;
6 months ago wenzelm 2019-03-28 clarified diagrams;
6 months ago wenzelm 2019-03-28 clarified diagrams;
6 months ago wenzelm 2019-03-28 proper syntax diagrams; tuned whitespace;
6 months ago wenzelm 2019-03-28 tuned names;
6 months ago wenzelm 2019-03-28 tuned whitespace;
6 months ago wenzelm 2019-03-28 proper local_theory command;
6 months ago wenzelm 2019-03-27 more exports: avoid clones in AFP;
6 months ago wenzelm 2019-03-27 tuned;
6 months ago wenzelm 2019-03-27 export_code/check_code formally updates the theory -- this opens further possibilities concerning Generated_Files; tuned;
6 months ago wenzelm 2019-03-27 tuned whitespace;
6 months ago wenzelm 2019-03-27 merged
6 months ago wenzelm 2019-03-27 more informative Spec_Rules.Equational: support corecursion;
6 months ago wenzelm 2019-03-27 more operations;
6 months ago paulson 2019-03-27 more stuff from HOL Light: Euclidean spaces and n-spheres, Hausdorff spaces, etc.
6 months ago wenzelm 2019-03-26 merged
6 months ago wenzelm 2019-03-26 more informative Spec_Rules.Equational, notably primrec argument types;
6 months ago wenzelm 2019-03-26 clarified signature: avoid direct comparison on type rough_classification;
6 months ago wenzelm 2019-03-26 tuned proofs;
6 months ago wenzelm 2019-03-26 removed spurious debugging;
6 months ago wenzelm 2019-03-26 export propositional status of consts;
6 months ago paulson 2019-03-26 merged
6 months ago paulson 2019-03-26 generalised homotopic_with to topologies; homotopic_with_canon is the old version
6 months ago Thomas Sewell 2019-03-26 follow up on Braun: get timing function right
6 months ago Thomas Sewell 2019-03-26 Tweak Braun tree list_fast_rec recursion. A minor adjustment simplifies the termination argument slightly.
6 months ago wenzelm 2019-03-25 more robust: avoid NPE due to odd problems with object initialization;
6 months ago wenzelm 2019-03-25 RDF meta data for AFP entries; tuned;
6 months ago wenzelm 2019-03-25 more strict AFP properties;
6 months ago wenzelm 2019-03-25 tuned signature;
6 months ago wenzelm 2019-03-25 clarified signature;
6 months ago wenzelm 2019-03-25 proper treatment of empty extra lines (amending 98a440cfbb2b);
6 months ago wenzelm 2019-03-25 clarified signature: explicitly typed interfaces;
6 months ago wenzelm 2019-03-25 provide maintainers as seen in AFP/admin; suppress empty properties;
6 months ago wenzelm 2019-03-25 tuned;
6 months ago wenzelm 2019-03-25 tuned signature;
6 months ago wenzelm 2019-03-25 read AFP metadata for entries;
6 months ago wenzelm 2019-03-24 more accurate HTML rendering;