Structured proofs in ZF

refined define_command vs. run_command: static tokenization vs. dynamic parsing, to increase the chance that the proper transaction is run after redefining commands (NB: requires slightly more space and time for document state);

updated polyml/build option to prefer included libffi;

tuned signature;

clarified prepare_positions: always retain source positions to allow using it as formal information, not just markup reports;

merged

renewing Executable_Relation

tuned;

more direct Name_Space.defined_entry; tuned Variable.export_inst: avoid keeping full contexts within the gen_fixesT closure (NB: locale infrastructure stores morphisms persistently);

eliminated old-fashioned 'constrains' element;

modernized locale expression, with some fluctuation of arguments;

simplified span class in conformance to Scala version;

discontinued specific entity markup, which causes confusion with "kind" names with spaces (e.g. "type name"); uniform treatment of "class" entities in input and output;

merged

adding tags to quickcheck's result

clarified idents for activated locales, with subtle change of semantics: insert/merge wrt. term equality, but avoid redundant_ident on retrieval; avoid confusing quasiorder ident_le as "eq" for member/merge;

eliminated dead code;

clarified total_ident_ord, swapping first argument back to normal (unlike e464f84f3680) -- NB: "fast" ord is erratic anyway;

misc tuning and simplification;

tuned;

clarified Pattern.matchess;

tuned;

more precise alignment of begin/end, proof/qed; improved English;

merged

beautified

more precise checking for wellformedness of mapper, before and after morphism application

reject mapper terms with type variables not contained in the term's type

always bracket case expressions in Scala

tuned signature;

merges

More calculation-based cardinality proofs

split make_tptp_parser into two scripts, for parser and lib respectively;

added ml-yacc library sources;

added tptp parser;

merged

Structured and calculation-based proofs (with new trans rules!)

Structured and calculation-based proofs (with new trans rules!)

tuned comment;

simplified -- plain map_index is sufficient (pointed out by Enrico Tassi);

tuned;

clarified XML signature (again) -- coincide with basic Markup without explicit dependency;

more precise warning/error positions;

merged

less rigorous but more realistic migration recommendation; note on code generation of sets

tuned syntax; more candidates

tuned message (cf. ML version);

eliminated dead code; tuned;

tuned signature;

simplified signature (NB: interpretation of properties is mainly done via XML.Encode/Decode);

to_pred/set attributes now properly handle variables of type "... => T set"

some recovery of IsaMakefile targets from f3c10e908f65;

added max_new_mono_instances, max_mono_iters, to Mirabelle-Sledgehammer; changed sh_minimize to avoid setting Mirabelle-level defaults;

added sh_minimize and preplay_timeout options to Mirabelle's Sledgehammer action;

added Mirabelle action info in its log file; tuned;

More mathematical symbols for ZF examples

mathematical symbols for Isabelle/ZF example theories

Using mathematical notation for <-> and cardinal arithmetic

mathematical symbols instead of ASCII

addressed a quotient-type-related issue that arose with the port to "set"

ensure no abstractions leak through after lambda-lifting (for formulas with higher-order occurrences of quantifiers)

updates for jedit-4.5.0 (still inactive);

more explicit patches;

tuned comment;

removed obsolete proper_command_at (cf. 03a2dc9e0624);

added Command.proper_range (still unused);

clarified special eol treatment and moved to gfx_range -- enables error messages at end of input, e.g. "prop PROP";

clarified command span: include trailing whitespace/comments and thus reduce number of ignored spans with associated transactions and states (factor 2); simplified signatures;

tuned

move test targets to test target

dropped images for importer sessions

dropped dead code

more accurate dependencies

tuned ML

dropped silly code

tuned

dropped dead code

actually add "the" Importer theory

avoid internal hol4 name references in generic importer code

generalized user-visible text

generalized attribute name

dropped dead theories

one unified Importer theory

added actual dependencies

import all importer theories in compatibility layer

merged;

dropped obsolete ROOT.ML

plugged in pre-existing theories appropriately

switch of target Import-HOL_Light-Imported: not operative at the moment

turn on quick and dirty in batch mode

tuned whitespace

file system structure separating HOL4 and HOL Light concerns

distribution of compatibility theories

formal infrastructure for import sessions

dropped dead code

tuned whitespace

spurious set/pred correction

explicit locations for import_theory and setup_theory, for better user interface conformance; spurious set/pred correction

explicit locations for import_theory and setup_theory, for better user interface conformance

discontinued obsolete Library.foldl_map and Library.apply (NB: apply = fold I);

tuned;

tuned;

tuned;

canonical argument order for attribute application;

clarified terminology of raw protocol messages;

tuned;

tuned signature -- emphasize Isabelle_Process Input vs. Output;

explicit syslog_limit reduces danger of low-level message flooding; tuned;

retain original "uses" (again) -- still required for Thy_Load.use_file etc. in ML (notably for maintaining required/provided); tuned;

clarified scope of exception handlers;

relevant timing as in ML; more PIDE modules;

more fundamental pred-to-set conversions for range and domain by means of inductive_set

merged

tuned whitespace

tuned import

dropped dead code

terminate after first exception -- avoid syslog flooding;

avoid buffer loading overrun; tuned;

merged

collecting all axioms in a locale context in quickcheck; adding some verbose output;

choosing longer constant names in Quickcheck_Narrowing to reduce the chances of name clashes in Quickcheck-Narrowing