changed name of interpretation linorder to order

adjusted to changes in class package

added outline for Isabelle library description

adjusted to new code generator Isar commands and changes in implementation

adjusted to new code generator Isar commands

added references for code generator tutorial

added antiquotation for exceptions

updated keywords

cterm_instantiate was calling a type instantiation function that works only for matching, not unification as here.

added get-functions

Renamed member to memb to avoid confusion with member function defined in Predicate theory.

Adapted to changes in Finite_Set theory.

Adapted to new inductive definition package.

- Adapted to new inductive definition package - Adapted to changes in Multiset theory

Added meta_spec to extraction_expand.

Added functions hhf_proof and un_hhf_proof.

Adapted to changes in Accessible_Part and Wellfounded_Recursion theories.

Added split_rule attribute.

Fixed bug in mk_AbsP.

Introduction and elimination rules for <= on predicates are now declared properly.

- Improved handling of monotonicity rules involving <= - ind_cases: variables to be generalized can now be specified using "for" keyword

Adapted to changes in Finite_Set theory.

Adapted to changes in Finite_Set theory.

- Adapted to new inductive definition package - More elegant proof of eta postponement theorem inspired by Andreas Abel

Adapted to new inductive definition package.

Converted to predicate notation.

Adapted to changes in List theory.

- wfP has been moved to theory Wellfounded_Recursion - Accessible part now works on predicates, hence accP is no longer needed

Adapted to changes in Transitive_Closure theory.

Adapted to new inductive definition package.

Adapted to changes in Finite_Set theory.

Theorems for converting between wf and wfP are now declared as hints.

- Adapted to new inductive definition package - Predicate version of wellfoundedness

Adapted to new inductive definition package.

Adapted to changes in Transitive_Closure theory.

Added Predicate theory.

New theory for converting between predicates and sets.

changes in lexicographic_order termination tactic

"prove" function now instantiates relation variable in order to avoid problems with higher-order unification. This allows relations to be encoded as binary predicates.

Made untabify function tail recursive.

tuned matches_subterm;

trace/debug: avoid eager string concatenation;

cc: removed option -lstdc++, which seems to be unnecessry, but causes problems on some platforms;

pervasive exception Option; fixed use_file;

added has_kind/get_kind; tuned;

fixed two stupid bugs of SML to do with the value restriction and missing type information in records

askids/qualified_thms_of_thy: version which returns names in domain of get_thm

added eta expansion to imperative monad bind

corrected typo introduced by me

now obsolete

moved the infrastructure from the nominal_tags file to nominal_thmdecls file, and adapted the code to conform with informal Isabelle programming conventions

Exporting curried versions of tail recursive equations instead of internal ones

proper use of NameSpace.is_qualified (avoids compatibility issues of the SML B library);

removed non-modular comment;

interpretation: attempt to be more serious about name_morphism;

added full_naming;

tuned oracle interface; simproc_setup: added identifier;

added print_strings;

old-fashioned abstype ctyp/cterm/thm prevents accidental equality tests;

def_simproc(_i): tuned interface; tuned simprocs environment;

added cterm interface;

type simproc: explicitl dependency of morphism; added eq_simproc, morph_simproc; renamed mk_simproc' to make_simproc -- primary interface;

load morphism.ML later;

added the two renaming functions from my PhD

added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user

a few additions and deletions

tuned;

proper use of PureThy.has_name_hint instead of hard-wired string'';

removed non-modular comment;

new theorem int_infinite

Fix tell_thm_deps to match changse in PureThy.

Expose hard-wired string which was changed and broke Proof General.

clarified error message

clarified command annotation

changed cong alist - now using AList operations instead of overwrite_warn

dropped Output.update_warn

print translation for record types with empty-sorted type variables raise Match instead of producing an error

dropped lemma duplicates in HOL.thy

Tidying; more debugging information. New reference unwanted_types.

Tweak preferences for PGIP interfaces. Make <askids> return theory successors instead of parents (ideally should be content elements).

Add get_succs

Add operations on preference tables (remove, set_default).

adjusted to new codegen_funcgr interface

added interface for plugging in preprocessors

additional auxiliary here

whitespace tuning

dropped dead code

shifted import order

dropped whitespace

changed name of interpretation linorder to order

proper simproc_setup; tuned ML setup;

added get_simproc, @{simproc};

added interface for target_naming;

added simproc_setup;

added def_simproc(_i) -- define named simprocs; tuned;

updated;