isabelle: Changelog

Mercurial Mercurial > repos > isabelle / changelog

Tue, 04 Jul 2006 15:30:29 +0200 tuned;

changeset

wenzelm [Tue, 04 Jul 2006 15:30:29 +0200] rev 19989

tuned;

Tue, 04 Jul 2006 15:30:28 +0200 added 'value';

changeset

wenzelm [Tue, 04 Jul 2006 15:30:28 +0200] rev 19988

added 'value'; tuned;

Tue, 04 Jul 2006 15:26:56 +0200 - put declarations inside a structure (NominalPermeq)

changeset

berghofe [Tue, 04 Jul 2006 15:26:56 +0200] rev 19987

- put declarations inside a structure (NominalPermeq) - dynamic_thm(s) now looks up theorems in theory associated with proof state (rather than in context associated with simpset) - finite_guess_tac now automatically adds some extra rules about supp to the simpset

Tue, 04 Jul 2006 15:22:54 +0200 - nominal_permeq.ML is now loaded before nominal_package.ML

changeset

berghofe [Tue, 04 Jul 2006 15:22:54 +0200] rev 19986

- nominal_permeq.ML is now loaded before nominal_package.ML - methods and tactics in nominal_permeq.ML are now defined inside structure NominalPermeq, therefore the names in the method_setup section had to be changed

Tue, 04 Jul 2006 15:20:43 +0200 Implemented proofs of equivariance and finite support

changeset

berghofe [Tue, 04 Jul 2006 15:20:43 +0200] rev 19985

Implemented proofs of equivariance and finite support for graph of recursion combinator.

Tue, 04 Jul 2006 14:47:01 +0200 Method intro_locales replaced by intro_locales and unfold_locales.

changeset

ballarin [Tue, 04 Jul 2006 14:47:01 +0200] rev 19984

Method intro_locales replaced by intro_locales and unfold_locales.

Tue, 04 Jul 2006 12:13:38 +0200 updated

changeset

urbanc [Tue, 04 Jul 2006 12:13:38 +0200] rev 19983

updated