misc tuning;

prefer existing beta_eta_conversion;

more standard fold/fold_rev;

tuned import;

misc tuning;

prefer existing beta_eta_conversion;

more standard names;

simplified method setup;

tuned -- prefer terminology of tactic / goal state;

tuned;

misc tuning;

tuned;

tuned signature;

stay within regular tactic language -- avoid operating on whole proof state;

standardized aliases;

space between minus sign and number for large negative number literals causes NumberFormatException at run-time

tuned

relational version of HoareT

obsolete;

resolve_inc_tyvars: back to old behavior before 0fa3b456a267 where types of equal Vars are *not* unified -- recover last example in src/HOL/Metis_Examples/Clausification.thy;

more precise "incremented" indication, which might be relevant in corner cases, e.g. instantiation of leading to vars with different types (which is a potential problem nonetheless);

tuned signature -- more explicit flags for low-level Thm.bicompose;

unify types of schematic variables in non-lifted case (i.e. "compose variants") -- allow schematic polymorphism, without revisiting HO-unification;

tuned signature;

backout 3b9c31867707 -- too risky to "amend" modules from 25 years ago that don't handle Vars with different types;

observe type annotations in print translations as well, notably type_constraint_tr';

make SML/NJ happy;

tuning

more work on general recursors

tuning (use lists rather than pairs of lists throughout)

generalized recursors, effectively reverting inductive half of c7a034d01936

tuning

merged

explicit support for type annotations within printed syntax trees; eliminated obsolete show_free_types;

more explicit Printer.type_emphasis, depending on show_type_emphasis; tuned signature;

tuning (refactoring)

refactored triplicated functionality

tuning -- avoided unreadable true/false all over the place for LFP/GFP

merge

don't create needless constant

merged

fixed broken Cardinals and BNF due to Order_Union

no confusing special behavior in debug mode

tuned Nitpick message to be in sync with similar warning from Kodkod

merged

merged Well_Order_Extension into Zorn

removed junk (cf. 667961fa6a60);

exported ML function

redid rac7830871177 to avoid duplicate fixed variable (e.g. lemma "P (a::nat)" proof - have "!!a::int. Q a" sledgehammer [e])

clean up list of theorems

removed needless comment (yes, sum_case_if is needed)

tuned

actually test theory Order_Union;

more direct notation;

merged

more literal tokens, e.g. "EX!";

report markup for ast translations;

tuned;

tuned;

discontinued obsolete show_all_types;

added Ordered_Union

fixed files broken due to Zorn changes (cf. 59e5dd7b8f9a)

well-order extension (by Christian Sternagel)

modernized Zorn (by Christian Sternagel)

merged

more thorough type unification: treat equal Vars like other atoms, otherwise unify type of term pair (not just accidental body_type of its head Vars);

instantiate types as well (see also Thm.first_order_match);

tuned;

updated to ProofGeneral-4.2;

uniform Term_Position.markers (cf. dbadb4d03cbc);

get rid of "show_all_types" in Nitpick

tuning

killed dead argument

tuning

generalized "mk_co_iter" to handle mutualized (co)iterators

tuning

tuned

tuned

merged

tuned

merged

position constraint for bound dummy -- more PIDE markup;

position constraint for dummy_pattern -- more PIDE markup;

tuned;

tuned signature;

tuned -- less ML compiler warnings;

more robust variant_free: avoid clash with consts name space (e.g. consts "x", "xa", etc.);

more uniform context;

tuned signature;

more conventional pretty printing; more markup;

tuned white-space;

more specific structure for registration into theory and dependency onto locale

examples for interpretation into target

disable SPASS's splitting if Isar proofs are desired, because these are not handled by the proof reconstruction code (and it's not clear how to handle them considering the lack of documentation)

handle lambda-lifted problems in Isar construction code

simpler proof through custom summation function

merged

tuned;

tuned;

tuned;

tuned;

syntax translations always depend on context;

updated keywords;

weaker precendence of syntax for big intersection and union on sets

tuned structure

add lemma

bookkeeping and input syntax for exact specification of names of symbols in generated code

use generic data for code symbols for unified "code_printing" syntax for custom serialisations

dedicated module for code symbol data

symbol data covers class relations also

merged

proper internal error, not user error;

tuned;

tuned signature;

tuned;

unify types of bound variables in the same manner as Unify.new_dpair (which emphatically "Tries to unify types of the bound variables!");

tuned signature -- slightly more general operations (cf. term.ML);

re-use Pattern.unify_types, including its trace_unify_fail option;

tuned signature; tuned comments;

improved handling of free variables' types in Isar proofs

pass noninteractive flag -- necessary to run under CASC's "runsolver" program

untabify

more lemmas for sorted_list_of_set

prefer object equality

slightly clearer formulation

interpretation must always operate on the last element in a local theory stack, not on all elements: interpretated facts must disappear after pop from local theory stack, and transfer from last target is not enough

mark local theory as brittle also after interpretation inside locales; more correct bookkeeping on brittleness: must store directly beside lthy data, with implicit default true for levels > 1; check brittleness only during context switch using (in ...) syntax, not for arbitrary exit of local theory

merged