Fix idvalue output and PGML print mode raw encode/decode.

permitting empty datatypes

improved handling of nat numerals

tuned code theorems for ord on integers

simplified code generator setup

tuned code theorems

added add_numerals_of

now using "class"

using "fst" "snd" for Haskell code

added code theorems for UNIV

adjusted to latest changes

new code theorems

syntax for "class attach const"

prefix of class interpretation not mandatory any longer

Meson.is_fol_term now takes a theory as argument. Minor tidying.

New code to store theorem names in a concise form rather than as fully-qualified. Meson.is_fol_term now takes a theory as argument.

The first-order test now tests for the obscure case of a polymorphic constant like 1 being used with a function type.

abbrev: be permissive after transformation;

exported get_ss, map_ss;

tuned;

tuned ML setup;

added @{const_name}, @{const_syntax};

more cleanup

Add closeblock/openblock structure to proof-block commands

Updated success string for Vampire. eprover no longer sought in the PROVER directory. eprover now gets tstp input. Streamlined the code a bit.

Now outputs metis calls

added headers

cleanup, fixing sml/nj related problems

gensym: removed bits of dead code;

gensym no longer includes ' or _ in names (trailing _ is bad)

tuned document;

\usepackage{amssymb};

moved some non-kernel material to more_thm.ML;

removed obsolete eq_set;

Thm.internalK;

Further operations on type thm, outside the inference kernel.

added more_thm.ML;

moved eq_thm etc. to structure Thm in Pure/more_thm.ML;

Added formalization of size-change principle (experimental).

added theorems_of;

removed obsolete theorem_space;

Added lemma lfp_const: "lfp (%x. t) = t

exported serializer parsers

proper treatment of -> as type constructor

tuned

add_path for naming in proof contexts

locale: add_locale accepts explicit predicate name, interpretation supports non-mandatory prefixes

slightly tuned

slight cleanup

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.