made SML/NJ happier

updated NEWS

merged

removed theory dependency of BNF_LFP on Datatype

made SML/NJ happier

removed dependency on 'Datatype' structure

made SML/NJ happier

compile

compile

technical import to avoid infamous 'duplicate Option.size' error at merge time in 'List.thy'

swapped dependencies of 'Finite_Set' and 'Option' (to move BNF up)

moved 'bacc' back to 'Enum' (cf. 744934b818c7) -- reduces baggage loaded by 'Hilbert_Choice'

renamed 'regular' to 'regularCard' to avoid clashes (e.g. in Meson_Test)

hide BNF notation

moved 'fundef_cong' attribute (and other basic 'fun' stuff) up the dependency chain

rationalized lemmas

move BNF_LFP up the dependency chain

compile

updated docs

have Nitpick lookup codatatypes

removed dependency of BNF package on Nitpick

deactivate one more cardinal notation

fixed typo

compile

dissolved BNF session

rationalized dependencies

reduced dependencies + updated docs

minimized Nitpick's dependencies

moved BNF examples

rationalized dependencies

moved hide_const from BNF to Main

updated README

tuned names

tuning

compile

killed obsolete session

tuned comment

made BNF compile after move to HOL

adjusted comments

avoid nested 'Tools' directories

tuned comments

moved BNF files to 'HOL'

kill notations

renamed '_FP' files to 'BNF_' files

tuning

moved subset of 'HOL-Cardinals' needed for BNF into 'HOL'

tuned names

spelling

killed obsolete provers from documentation

merged

removed obsolete remote_cvc3 and remote_z3

implicit "cartouche" method (experimental, undocumented);

more examples;

cartouche within antiquotation;

cartouche within nested args (attributes, methods, etc.);

group symbols;

prefer indexes user for pattern matching to print concrete names for symbols, do not rely on printable unique identifiers

table for code symbols

HTML output for \<newline>;

sorted entries according to components_checksum;

more unicode tokens; diff -r ProofGeneral-4.2/isar/isar-unicode-tokens.el ProofGeneral-4.2-1/isar/isar-unicode-tokens.el 356c356,359 < ("some" "ϵ")) --- > ("some" "ϵ") > ("open" "‹") > ("close" "›") > ("newline" "⏎"))

prefer Isar commands over old-fashioned ML (see also a189c6274c7a); removed pointless space: the second "_ \<Colon> _" should take precendence anyway;

crude latex macro for \<newline;

proper \<newline>;

unused;

tuned;

support for nested text cartouches; clarified Symbol.is_symbolic: exclude \<open> and \<close>;

back to conditional tracing instead of noisy warning (see also 00e849f5b397): these incidents happen occasionally;

tuned;

prefer user-space tool within Pure.thy;

clarified @{rail} syntax: prefer explicit \<newline> symbol;

clarified Simplifier diagnostics -- simplified ML; unconditional warning for structural mistakes (NB: context of running Simplifier is not visible, and cond_warning ineffective);

folded 'Wellfounded_More_FP' into 'Wellfounded'

folded 'Order_Relation_More_FP' into 'Order_Relation'

support declaration of nonemptiness witnesses in bnf_decl

hide short const name

get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'

liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts

compile (importing 'Metis' or 'Main' would have been an alternative)

dissolved 'Fun_More_FP' (a BNF dependency)

moved lemmas from 'Fun_More_FP' to where they belong

moved 'Zorn' into 'Main', since it's a BNF dependency

adapted to move of Wfrec

moved Wfrec to Main, since it is a dependency of cardinals, hence BNFs

added \<newline> symbol, which is used for char/string literals in HOL;

general notion of auxiliary bounds within context; revert_bounds as part of regular unparse_term; avoid special variants of Syntax.string_of_term in Simplifier (e.g. relevant for add-on tracing);

merged

fall-back on old Z3_NON_COMMERCIAL, which simplifies automatic test environments like isatest and mira;

tuned text

tuned

automatically solve proof obligations produced for code equations

use 'disc_exhausts' property both from types on which 'case's take place and on return type

activation of Z3 via "z3_non_commercial" system option (without requiring restart);

tuned;

use the right context in 'unfold_thms id_def'

repaired 'ctr' tactic w.r.t. 'split'