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.