isabelle: Changelog

Mercurial Mercurial > repos > isabelle / changelog

Mon, 17 Oct 2005 23:10:17 +0200 functor: no Simplifier argument;

changeset

wenzelm [Mon, 17 Oct 2005 23:10:17 +0200] rev 17879

functor: no Simplifier argument; export change_clasimpset;

Mon, 17 Oct 2005 23:10:16 +0200 tuned;

changeset

wenzelm [Mon, 17 Oct 2005 23:10:16 +0200] rev 17878

tuned;

Mon, 17 Oct 2005 23:10:15 +0200 Simplifier.inherit_context instead of Simplifier.inherit_bounds;

changeset

wenzelm [Mon, 17 Oct 2005 23:10:15 +0200] rev 17877

Simplifier.inherit_context instead of Simplifier.inherit_bounds;

Mon, 17 Oct 2005 23:10:13 +0200 change_claset/simpset;

changeset

wenzelm [Mon, 17 Oct 2005 23:10:13 +0200] rev 17876

change_claset/simpset;

Mon, 17 Oct 2005 23:10:10 +0200 change_claset/simpset;

changeset

wenzelm [Mon, 17 Oct 2005 23:10:10 +0200] rev 17875

change_claset/simpset; Simplifier.inherit_context instead of Simplifier.inherit_bounds;

Mon, 17 Oct 2005 19:19:29 +0200 Improved proof of injectivity theorems to make it work on

changeset

berghofe [Mon, 17 Oct 2005 19:19:29 +0200] rev 17874

Improved proof of injectivity theorems to make it work on "ordinary" function types as well.

Mon, 17 Oct 2005 18:34:51 +0200 Fixed bug in proof of support theorem (it failed on constructors with no arguments).

changeset

berghofe [Mon, 17 Oct 2005 18:34:51 +0200] rev 17873

Fixed bug in proof of support theorem (it failed on constructors with no arguments).

Mon, 17 Oct 2005 17:42:24 +0200 Implemented proofs for support and freshness theorems.

changeset

berghofe [Mon, 17 Oct 2005 17:42:24 +0200] rev 17872

Implemented proofs for support and freshness theorems.

Mon, 17 Oct 2005 17:40:34 +0200 deleted leading space in the definition of fresh

changeset

urbanc [Mon, 17 Oct 2005 17:40:34 +0200] rev 17871

deleted leading space in the definition of fresh

Mon, 17 Oct 2005 12:30:57 +0200 Initial revision.

changeset

berghofe [Mon, 17 Oct 2005 12:30:57 +0200] rev 17870

Initial revision.

Sat, 15 Oct 2005 00:14:30 +0200 tuned;

changeset

wenzelm [Sat, 15 Oct 2005 00:14:30 +0200] rev 17869

tuned;

Sat, 15 Oct 2005 00:09:20 +0200 tuned comment;

changeset

wenzelm [Sat, 15 Oct 2005 00:09:20 +0200] rev 17868

tuned comment;

Sat, 15 Oct 2005 00:09:07 +0200 added ML_type, ML_struct;

changeset

wenzelm [Sat, 15 Oct 2005 00:09:07 +0200] rev 17867

added ML_type, ML_struct;

Sat, 15 Oct 2005 00:08:15 +0200 more;

changeset

wenzelm [Sat, 15 Oct 2005 00:08:15 +0200] rev 17866

more;

Sat, 15 Oct 2005 00:08:14 +0200 * antiquotations ML_type, ML_struct;

changeset

wenzelm [Sat, 15 Oct 2005 00:08:14 +0200] rev 17865

* antiquotations ML_type, ML_struct; * Isar 'guess' element;

Sat, 15 Oct 2005 00:08:13 +0200 added guess;

changeset

wenzelm [Sat, 15 Oct 2005 00:08:13 +0200] rev 17864

added guess;

Sat, 15 Oct 2005 00:08:12 +0200 added antiquotations ML_type, ML_struct;

changeset

wenzelm [Sat, 15 Oct 2005 00:08:12 +0200] rev 17863

added antiquotations ML_type, ML_struct;

Sat, 15 Oct 2005 00:08:11 +0200 use perl for test/stat;

changeset

wenzelm [Sat, 15 Oct 2005 00:08:11 +0200] rev 17862

use perl for test/stat;

Sat, 15 Oct 2005 00:08:10 +0200 export strip_params;

changeset

wenzelm [Sat, 15 Oct 2005 00:08:10 +0200] rev 17861

export strip_params;

Sat, 15 Oct 2005 00:08:09 +0200 note_thmss, read/cert_vars etc.: natural argument order;

changeset

wenzelm [Sat, 15 Oct 2005 00:08:09 +0200] rev 17860

note_thmss, read/cert_vars etc.: natural argument order; added string_of_thm; tuned;

Sat, 15 Oct 2005 00:08:08 +0200 goal statements: before_qed argument;

changeset

wenzelm [Sat, 15 Oct 2005 00:08:08 +0200] rev 17859

goal statements: before_qed argument;

Sat, 15 Oct 2005 00:08:07 +0200 added 'guess', which derives the obtained context from the course of reasoning;

changeset

wenzelm [Sat, 15 Oct 2005 00:08:07 +0200] rev 17858

added 'guess', which derives the obtained context from the course of reasoning;

Sat, 15 Oct 2005 00:08:06 +0200 added primitive_text, succeed_text;

changeset

wenzelm [Sat, 15 Oct 2005 00:08:06 +0200] rev 17857

added primitive_text, succeed_text;

Sat, 15 Oct 2005 00:08:05 +0200 goal statements: accomodate before_qed argument;

changeset

wenzelm [Sat, 15 Oct 2005 00:08:05 +0200] rev 17856

goal statements: accomodate before_qed argument; ProofContext.note_thmss_i: natural argument order;

Sat, 15 Oct 2005 00:08:04 +0200 goal statements: accomodate before_qed argument;

changeset

wenzelm [Sat, 15 Oct 2005 00:08:04 +0200] rev 17855

goal statements: accomodate before_qed argument;

Sat, 15 Oct 2005 00:08:03 +0200 added 'guess';

changeset

wenzelm [Sat, 15 Oct 2005 00:08:03 +0200] rev 17854

added 'guess';

Sat, 15 Oct 2005 00:08:02 +0200 tuned;

changeset

wenzelm [Sat, 15 Oct 2005 00:08:02 +0200] rev 17853

tuned;

Sat, 15 Oct 2005 00:08:01 +0200 added no_facts;

changeset

wenzelm [Sat, 15 Oct 2005 00:08:01 +0200] rev 17852

added no_facts;

Sat, 15 Oct 2005 00:08:00 +0200 tuned comments;

changeset

wenzelm [Sat, 15 Oct 2005 00:08:00 +0200] rev 17851

tuned comments;

Sat, 15 Oct 2005 00:07:59 +0200 updated;

changeset

wenzelm [Sat, 15 Oct 2005 00:07:59 +0200] rev 17850

updated;

(0) -10000 -3000 -1000 -300 -100 -50 -30 +30 +50 +100 +300 +1000 +3000 +10000 +30000 tip

isabelle

RSS Atom