adjusted code lemmas

continued

dropped diagnostic switch

Improved handling of situation when theorem in cache disagrees with theorem supplied: new clauses are now returned, fixing a bug in the metis method.

Fixed print translations for quantifiers a la "ALL x>=t. P x". These used to fail when the other term in the comparison was itself a bound variable, as in "EX y. ALL x>=y. P x".

prevent quadratic time removal of duplicates if filter list is empty (likely to have too many results)

added missing \

updated docs with new with_dups syntax for find_theorems

Remove duplicates from printed theorems in find_theorems (still pretty slow, needs optimising). Added syntax "find_theorems (..) with_dups .." to switch off removal.

more precise error message in parameter unification

Updated

Fix <pgipquit>. Remove unused pgmlatomsN. Make showid match askids. Use string functions for showid, avoiding printwrap kludge.

<idvalue>: add name attribute to allow unsolicited updates.

pretty_full_theory: expose in signature.

Clarify comment

unified arity parser/arguments;

ML text: informative Output.debug only;

unified arity parser/arguments;

Replaced "raise RecError" by "primrec_err" in function gen_primrec_i to prevent error message from being suppressed.

added example for print-mode Axiom

added print-mode Axiom to print theorems without premises with a rule on top.

updated Makefile

start adding the attribute eqvt to some lemmas of the nominal library

changed termination goal to use object quantifier

added congruence rule for function composition

beta_eta_contract specification befor processing. These normal forms avoid unpleasant surprises later on.

continued

class package now using Locale.interpretation_i

clarified explanation

cleanup

simpliefied instance statement

continued class tutorial

added class "preorder"

Added nominal_inductive keyword.

Added new file Nominal/nominal_inductive.ML

First steps towards strengthening of induction rules for inductively defined predicates involving nominal datatypes.

Added new file nominal_inductive.ML

Curried and exported mk_perm.

COMP now performs a distinctness check on the multiple results before failing

improved lexicographic order termination tactic

added OCaml example

Completing the bug fix from the previous update: the result of unifying type variables must be normalized WRT itself; otherwise instantiation is wrong

changed representation of constants; consistent name handling

changed representation of constants

tuned

new Isar command print_codesetup

added experimental class target

added class target stub

internal interfaces for interpretation and interpret

moved commands of class package here

added class package to Isar bootstrap

splut up code generation in two parts

canonical interface for attributes

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;