honor user-specified name for map function

honor user-specified set function names

parse set function name

merged

tuned

took out workaround for bug fixed in 5af40820948b

merged

slightly more aggressive syntax translation for printing case expressions

avoid odd reinit after sublocale declaration

moved defs into locale to reduce unnecessary polymorphism; tuned

dropped dead code

documentation and NEWS

avoid accidental specialization of the types in the "map" property of codatatypes

simplify "Inl () = Inr ()" as well (not entirely clear why this is necessary)

more examples

tuning

fix bugs in expand tactic w.r.t. datatypes with "needless" discriminators (e.g. lists with is_Nil instead of ~= Nil)

tuning

tuned_comment

(co)rec is (just as the (un)fold) the unique morphism;

tuned: unnamed contexts, interpretation and sublocale in locale target; corrected slip in List.thy: setsum requires commmutativity

target-sensitive user-level commands interpretation and sublocale

ML interfaces for various kinds of interpretation

brittleness stamping for local theories

tuned

removed type constraints

NEWS

more sharing

interpretation: distinguish theories and proofs by explicit parameter rather than generic context; formal initialisation of theory target during interpretation; prefer Local_Theory.notes_kind to register mixin equations during interpretation; more uniformity between note_eqns_register and note_eqns_dependency

dropped unusued identifier

avoid odd bifurcation with Attrib.local_notes vs. Locale.add_thmss -- n.b. note_eqns_dependency operates in a specific locale target

tuned for uniformity

reflection as official HOL tool

follow Isabelle spacing praxis more thoroughly

honour FIXMEs as far as feasible at the moment

combined reify_data.ML into reflection.ML; attempt to establish a more accessible and more consistent terminology; more ML code in ML file rather than setup theory; ML slightly tuned wrt. Isabelle coding conventions

proved termination for fun-based AI

tuned

tuned

merged

tuned signature;

simplifier uses proper Proof.context instead of historic type simpset;

merged

avoided map_of in def of fun_rep (but still needed for efficient code)

spelling

spelling

tuned

complete revision: finally got rid of annoying L-predicate

moved leastness lemma

proper prolog command-line instead of hashbang, which might switch to invalid executable and thus fail (notably on lxbroy2); speculative update for yap (untested);

use automatic type coerctions in Sqrt example

make SML/NJ happy;

not all Nitpick 'constructors' are injective -- careful

added another definition snipped

actually fail on prolog errors -- such as swipl startup failure due to missing shared libraries -- assuming it normally produces clean return code 0;

modifiers for classical wrappers operate on Proof.context instead of claset;

removed historic comments;

tuned exceptions -- avoid composing error messages in low-level situations;

tuned signature; tuned comments;

proper identifiers -- avoid crash of case translations;

reduced duplication

do not add case translation syntax in rep_datatype compatibility mode

run type inference on input to wrap_data

installed case translations in BNF package

tuned

more antiquotations;

tuned pretty layout: avoid nested Pretty.string_of, which merely happens to work with Isabelle/jEdit since formatting is delegated to Scala side; declare command "print_case_translations" where it is actually defined;

updated keywords;

merged

merged

obsolete -- tools should refer to proper Proof.context;

discontinued obsolete ML antiquotation @{claset};

added ML antiquotation @{theory_context};

more standard module name Axclass (according to file name);

made SML/NJ happy

generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector

NEWS and CONTRIBUTORS

declaration attribute for case combinators

Handle dummy patterns in parse translation rather than check phase

disallow coercions to interfere with case translations

allow redundant cases in the list comprehension translation

recur in the expression to be matched (do not rely on repetitive execution of a check phase); separate ML-interface function that is not recurring (strip_case)

tuned whitespace

Use Type.raw_match instead of Sign.typ_match

special constant to prevent eta-contraction of the check-phase syntax of case translations

separate data used for case translation from the datatype package

case translations performed in a separate check phase (with adjustments by traytel)

formal proof context for axclass proofs; avoid global_simpset_of -- refer to simpset of proof context;

prefer local context;

proper proof context; removed historic comments;

tuned;

merged

add command timings (like document command status);

tuned signature;

public Isabelle_Process.xml_cache (thread-safe); cache derived status messages;

tuned signature;

just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;

clarified protocol_message undefinedness;

quote by Alan Kay;

more accurate documentation;

discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems'; print timing as tracing, to keep it out of the way in Proof General; no timing of control commands, especially relevant for Proof General;

more accurate documentation of "(structure)" mixfix;

more robust static structure reference, avoid dynamic Proof_Context.intern_skolem in Syntax_Phases.decode_term;

tuned comment;

just one syntax category "mixfix" -- check structure annotation semantically;

tuned message;

handle case clashes on Mac file system by encoding goal numbers

avoid duplicate "tcon_" names

smoothly handle cyclic graphs

compile + fixed naming convention

reverted accidental changes to theory file + updated wrt ML file

no need to filter tautologies anymore -- they are prefiltered by "all_facts"'

work on CASC LTB ISA exporter

tuning

add continuous_on rules for products

fixed spelling

move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative

remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)

improved printing of exception CTERM (see also d0f0f37ec346);

prefer pretty_exn where possible -- NB: low-level General.exnMessage may still be used elsewhere (e.g. by the ML compiler itself);