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;