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.

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;

load morphism.ML later;

added the two renaming functions from my PhD

added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user

a few additions and deletions

tuned;

proper use of PureThy.has_name_hint instead of hard-wired string'';

removed non-modular comment;

new theorem int_infinite

Fix tell_thm_deps to match changse in PureThy.

Expose hard-wired string which was changed and broke Proof General.

clarified error message

clarified command annotation

changed cong alist - now using AList operations instead of overwrite_warn

dropped Output.update_warn

print translation for record types with empty-sorted type variables raise Match instead of producing an error

dropped lemma duplicates in HOL.thy

Tidying; more debugging information. New reference unwanted_types.

Tweak preferences for PGIP interfaces. Make <askids> return theory successors instead of parents (ideally should be content elements).

Add get_succs

Add operations on preference tables (remove, set_default).

adjusted to new codegen_funcgr interface

added interface for plugging in preprocessors

additional auxiliary here

whitespace tuning

dropped dead code

shifted import order

dropped whitespace

changed name of interpretation linorder to order

proper simproc_setup; tuned ML setup;

added get_simproc, @{simproc};

added interface for target_naming;

added simproc_setup;

added def_simproc(_i) -- define named simprocs; tuned;

updated;

Now deals with simples cases where the input equations contain type variables See example in ReflectionEx.thy

refined algorithm

clarified code

exported interface for explicit error messages

added NestedEnvironment

Improved debugging

Streamlined and improved debugging messages

more fixes of arithmetic for min/max.

min/max lemmas (actually unused!)

simplification of Suc/numeral combinations with min, max

Fixed long-standing, MAJOR bug in "lt"

adjusted manual to improved treatment of overloaded constants

Allows evaluation of min/max o numerals.

fixed bug for OCaml bigints

tuned

added explicit maintainance of coregular code theorems for overloaded constants

dropped useless stuff

clarified code

added explicit query function for arities to subalgebra projection

not importing NestedEnvironment

adjusted to changes in class package

made executable

improved

fxied bug for OCaml bigints

adjusted names

tuned eta_contract;

updated timing;

some new lemmas

Let <loadfile> execute even while a file is open interactively.

fixes smlnj-related problem, updated signature

added a fold up and fold down as separate functions and fixed zipto to use the folddown.

simplified proofs

Included ex/Fundefs.thy in HOL-ex session

* Preliminary implementation of tail recursion * Clarified internal interfaces

Add location_of_position. Needs work elsewhere.

Test askref

Expose currently open file

Sync location with pgip.rnc, fixing attribute names

Add askrefs, setrefs, error_with_pos

Comments

Comment

Add line_of, name_of destructors.

Added lemma nat_size[simp]: "size (n::nat) = n"

tuned;