flipped fold implementation

merged

codegen

code for {x:A. P(x)} and for fold

Testfile for Stefan's code generator

moved value.ML to src/Tools

\underscoreoff is now default

tuned some proofs

removed Ids;

merged

merged

merged

Unified syntax of nominal_primrec with the one used by fun(ction) and new version of primrec command.

Modified nominal_primrec to make it work with local theories, unified syntax with the one used by fun(ction) and new version of primrec command.

merged

tuned comments; tuned;

tuned ML_OPTIONS for improved multicore performance;

refined identity and ancestry: explicit draft flat, ids are unnamed, name consistency is checked for ancestry; tuned history: renamed version to stage, disallow checkpoint/finish_thy on finished theories; added display_names -- user-level presentation; removed obsolete exists_name, names_of; tuned;

requires: check ancestors directly;

Context.display_names;

global_qed: refrain from ProofContext.auto_bind_facts, to avoid polluting the final result context with bindings involving loose free variables;

usage: echo ML settings as well;

future proofs: more robust check via Future.enabled;

removed former Isabelle font (cf. IsabelleItalic);

incorporated isabelle-fonts side-branch (forced merge);

replaced single quote by mathematical prime;

generated file;

bold version: math glyphs from plain IsabelleMono;

fixed rangle;

use dash from text font, not math;

added glyphs for \<A> (cal), \<a> (rm), \<AA> (\frak), \<aa> (frak); replaced old-style digits by bold ones (bf);

generated ttf;

renamed to IsabelleMono;

added README with original licenses;

renamed Isabelle to IsabelleItalic;

fixed rangle glyph;

the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;

Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);

Isabelle font, based on TeX glyhps;

enable future_scheduler by default;

ISABELLE_USEDIR_OPTIONS: -M max is default;

unified ids for ancestors and checkpoints, removed obsolete history of checkpoints; tuned representation of internal node names -- avoid string copies; tuned signature;

removed spurious exception_trace;

print_theorems: more robust difference, even after finished proof;

export context_node;

merged

more antiquotations;

pcpodef package: state two goals, instead of encoded conjunction;

recovered goal_pat;

inhabitance goal is now stated in original form and result contracted -- the previous attempt with contracted goal and initial unfolding did not work, because it disrupted the Isar proof structure (e.g. ?thesis);

tuned signature: pcpodef_proof, pcpodef_proof_cmd etc.; more antiquotations; explicit Theory.requires; adapted to recent changes in ~~/src/HOL/Tools/typedef_package.ML; misc tuning and simplification;

add_typedef: unfold set_def in tactical proof as well;

merged

Theory.checkpoint before commencing proof;

misc tuning and modernisation;

merged

logically separate typedef axiomatization from constant definition

add def before setting up goal

killed dead code

constrain type inference to sort "type"

merged.

cleaned up some proofs in Cfun.thy

implement cont_proc theorem cache using theory data

use ML antiquotations

clean up diff_bin_simps

move nat_{div,mod}_distrib from NatBin to IntDiv, simplified proofs

fixed import: requires ContNotDenum;

fixed import: requires ContNotDenum;

requires RComplete;

merged.

move all neg-related lemmas to NatBin; make type of neg specific to int

separate neg_simps from rel_simps

use {less,le}_number_of in integer simprocs

use lemma lists defined in Int.thy

Merged.

Satisfy a_axioms.

Merged.

Enable keyword 'structure' in for clause of locale expression.

Correct order of defines in specification.

Pass on defines in inheritance; reject illicit defines created by instantiation.

Order of implicit parameters in locale expression.

NewLocale.intro_locales_tac added to Class.default_intro_tac.

When adding locales, delay notes until local theory is built.

merged

moved ContNotDenum into Library

move lemmas from Numeral_Type.thy to other theories

instantiation option :: (enum) enum

instance inat :: semiring_char_0

Default names for definitions.

Proper shape of assumptions generated from Defines elements.

Merged.

Explicitly close up defines.

Interpretation in proof contexts.

tuned LaTeX files

tuned LaTeX files

merged.

multiplication for type inat

fix proofs

change lemmas to avoid using neg

simplify less_nat_number_of

add lemma le_nat_number_of

merged

adapted to changes in binding module

merged

Name.name_of -> Binding.base_name

corrected theory path

removed Table.extend, NameSpace.extend_table

renamed force_proof to join_proof;

renamed force_proofs to join_proofs;

finish_thy: to not collapse checkpoints -- allows future proofs to be deferred indefinitely (performance tradeoff: 5-15% slowdown in sequential batch jobs);

improved future_schedule: more robust handling of failed parents (explicit join), final join of all futures, including Exn.release_all;

excursion: improve parallelism by not joining proofs here (depends on persistent checkpoints);

added new_task;

added constant value;

refined type deriv: replaced all_promises by max_promise (dependency limit) and open_promises (potentially unfinished/failed promises); name_thm: actually maintain max_promise/open_promises here (!), reduce open_promises as far as possible; tuned;

uniform treatment of ISABELLE_HOME/contrib vs. ISABELLE_HOME/..;

Merged.

Interpretation in theories including interaction with subclass relation.

merged

dropped NameSpace.declare_base