isabelle: Changelog

Mercurial Mercurial > repos > isabelle / changelog

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
(0) -10000 -3000 -1000 -300 -100 -50 -32 +32 +50 +100 +300 +1000 +3000 +10000 +30000 tip

Thu, 13 Apr 2006 12:01:04 +0200 moved print_theorems/theory to Isar/proof_display.ML;

wenzelm [Thu, 13 Apr 2006 12:01:04 +0200] rev 19426

moved print_theorems/theory to Isar/proof_display.ML;

Thu, 13 Apr 2006 12:01:03 +0200 added dest_conjunction_list;

wenzelm [Thu, 13 Apr 2006 12:01:03 +0200] rev 19425

added dest_conjunction_list; close_form: canonical order of variables;

Thu, 13 Apr 2006 12:01:02 +0200 export unflat (again);

wenzelm [Thu, 13 Apr 2006 12:01:02 +0200] rev 19424

export unflat (again);

Thu, 13 Apr 2006 12:01:01 +0200 use conjunction stuff from conjunction.ML;

wenzelm [Thu, 13 Apr 2006 12:01:01 +0200] rev 19423

use conjunction stuff from conjunction.ML;

Thu, 13 Apr 2006 12:01:00 +0200 expand_atom: Type.raw_match;

wenzelm [Thu, 13 Apr 2006 12:01:00 +0200] rev 19422

expand_atom: Type.raw_match;

Thu, 13 Apr 2006 12:00:59 +0200 added equal_elim_rule2;

wenzelm [Thu, 13 Apr 2006 12:00:59 +0200] rev 19421

added equal_elim_rule2; export dest_binop; export store_thm etc; moved conjunction stuff to conjunction.ML;

Thu, 13 Apr 2006 12:00:58 +0200 tuned comment;

wenzelm [Thu, 13 Apr 2006 12:00:58 +0200] rev 19420

tuned comment;

Thu, 13 Apr 2006 12:00:56 +0200 ignore sorts of consts declarations;

wenzelm [Thu, 13 Apr 2006 12:00:56 +0200] rev 19419

ignore sorts of consts declarations;

Thu, 13 Apr 2006 12:00:55 +0200 reworded add_axclass(_i): canonical specification format,

wenzelm [Thu, 13 Apr 2006 12:00:55 +0200] rev 19418

reworded add_axclass(_i): canonical specification format, purely definitional version, always qualify intro/axioms;

Thu, 13 Apr 2006 12:00:54 +0200 added conjunction.ML;

wenzelm [Thu, 13 Apr 2006 12:00:54 +0200] rev 19417

added conjunction.ML;

Thu, 13 Apr 2006 12:00:53 +0200 Meta-level conjunction.

wenzelm [Thu, 13 Apr 2006 12:00:53 +0200] rev 19416

Meta-level conjunction.

Thu, 13 Apr 2006 12:00:51 +0200 added conjunction.ML;

wenzelm [Thu, 13 Apr 2006 12:00:51 +0200] rev 19415

added conjunction.ML; tuned;

Thu, 13 Apr 2006 12:00:50 +0200 Sign.typ_equiv;

wenzelm [Thu, 13 Apr 2006 12:00:50 +0200] rev 19414

Sign.typ_equiv;

Thu, 13 Apr 2006 11:22:44 +0200 added subversion treatment

haftmann [Thu, 13 Apr 2006 11:22:44 +0200] rev 19413

added subversion treatment

Tue, 11 Apr 2006 16:00:09 +0200 classes: prefer thy operations;

wenzelm [Tue, 11 Apr 2006 16:00:09 +0200] rev 19412

classes: prefer thy operations; accomodate tuned interfaces of Logic/Sign/AxClass;

Tue, 11 Apr 2006 16:00:08 +0200 export pretty_classrel/arity;

wenzelm [Tue, 11 Apr 2006 16:00:08 +0200] rev 19411

export pretty_classrel/arity;

Tue, 11 Apr 2006 16:00:07 +0200 'axclass': no parameters;

wenzelm [Tue, 11 Apr 2006 16:00:07 +0200] rev 19410

'axclass': no parameters;

Tue, 11 Apr 2006 16:00:06 +0200 tuned;

wenzelm [Tue, 11 Apr 2006 16:00:06 +0200] rev 19409

tuned;

Tue, 11 Apr 2006 16:00:05 +0200 removed superclasses (see sign.ML);

wenzelm [Tue, 11 Apr 2006 16:00:05 +0200] rev 19408

removed superclasses (see sign.ML);

Tue, 11 Apr 2006 16:00:03 +0200 added super_classes (from sorts.ML);

wenzelm [Tue, 11 Apr 2006 16:00:03 +0200] rev 19407

added super_classes (from sorts.ML); removed read/cert_classrel (see axclass.ML);

Tue, 11 Apr 2006 16:00:02 +0200 added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);

wenzelm [Tue, 11 Apr 2006 16:00:02 +0200] rev 19406

added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML); tuned;

Tue, 11 Apr 2006 16:00:01 +0200 moved abstract syntax operations to logic.ML;

wenzelm [Tue, 11 Apr 2006 16:00:01 +0200] rev 19405

moved abstract syntax operations to logic.ML; maintain class parameters; added params_of_sort; added cert/read_classrel (from sign.ML), check class parameters; tuned;

Mon, 10 Apr 2006 16:00:34 +0200 Moved stuff from Ring_and_Field to Matrix

obua [Mon, 10 Apr 2006 16:00:34 +0200] rev 19404

Moved stuff from Ring_and_Field to Matrix

Mon, 10 Apr 2006 14:37:23 +0200 Adapted to changed type of add_typedef_i.

berghofe [Mon, 10 Apr 2006 14:37:23 +0200] rev 19403

Adapted to changed type of add_typedef_i.

Mon, 10 Apr 2006 11:35:02 +0200 Hoare(Parallel) dependencies on document/*

nipkow [Mon, 10 Apr 2006 11:35:02 +0200] rev 19402

Hoare(Parallel) dependencies on document/*

Mon, 10 Apr 2006 11:34:15 +0200 added references

nipkow [Mon, 10 Apr 2006 11:34:15 +0200] rev 19401

added references

Mon, 10 Apr 2006 11:33:36 +0200 Minimal doc

nipkow [Mon, 10 Apr 2006 11:33:36 +0200] rev 19400

Minimal doc

Mon, 10 Apr 2006 11:33:22 +0200 Included cyclic list examples

nipkow [Mon, 10 Apr 2006 11:33:22 +0200] rev 19399

Included cyclic list examples

Mon, 10 Apr 2006 08:30:26 +0200 fixed value restriction

haftmann [Mon, 10 Apr 2006 08:30:26 +0200] rev 19398

fixed value restriction

Mon, 10 Apr 2006 08:26:26 +0200 Added splicing algorithm.

nipkow [Mon, 10 Apr 2006 08:26:26 +0200] rev 19397

Added splicing algorithm.

Mon, 10 Apr 2006 00:34:46 +0200 hide (open) const;

wenzelm [Mon, 10 Apr 2006 00:34:46 +0200] rev 19396

hide (open) const;

Mon, 10 Apr 2006 00:33:54 +0200 simplified AxClass.add_axclass interface;

wenzelm [Mon, 10 Apr 2006 00:33:54 +0200] rev 19395

simplified AxClass.add_axclass interface;

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

isabelle