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