isabelle: Changelog

Mercurial Mercurial > repos > isabelle / changelog

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

Fri, 01 Oct 1999 20:41:58 +0200 fixed no_qed;

wenzelm [Fri, 01 Oct 1999 20:41:58 +0200] rev 7681

fixed no_qed;

Fri, 01 Oct 1999 20:40:03 +0200 added Isar/obtain.ML;

wenzelm [Fri, 01 Oct 1999 20:40:03 +0200] rev 7680

added Isar/obtain.ML;

Fri, 01 Oct 1999 20:39:40 +0200 improved 'fix' / Skolem interfaces;

wenzelm [Fri, 01 Oct 1999 20:39:40 +0200] rev 7679

improved 'fix' / Skolem interfaces;

Fri, 01 Oct 1999 20:38:50 +0200 added 'obtain' command;

wenzelm [Fri, 01 Oct 1999 20:38:50 +0200] rev 7678

added 'obtain' command;

Fri, 01 Oct 1999 20:38:16 +0200 tuned comment;

wenzelm [Fri, 01 Oct 1999 20:38:16 +0200] rev 7677

tuned comment;

Fri, 01 Oct 1999 20:38:00 +0200 added prf_asm_goal;

wenzelm [Fri, 01 Oct 1999 20:38:00 +0200] rev 7676

added prf_asm_goal;

Fri, 01 Oct 1999 20:37:38 +0200 added atomic_thesis;

wenzelm [Fri, 01 Oct 1999 20:37:38 +0200] rev 7675

added atomic_thesis;

Fri, 01 Oct 1999 20:36:53 +0200 The 'obtain' language element -- achieves (eliminated) existential

wenzelm [Fri, 01 Oct 1999 20:36:53 +0200] rev 7674

The 'obtain' language element -- achieves (eliminated) existential quantification proof command level.

Fri, 01 Oct 1999 18:36:12 +0200 added undef_global_attribute, undef_local_attribute;

wenzelm [Fri, 01 Oct 1999 18:36:12 +0200] rev 7673

added undef_global_attribute, undef_local_attribute;

Fri, 01 Oct 1999 10:23:13 +0200 - Fixed bug in mk_split_pack which caused application of expansion theorem

berghofe [Fri, 01 Oct 1999 10:23:13 +0200] rev 7672

- Fixed bug in mk_split_pack which caused application of expansion theorem to fail because of typing reasons - Rewrote inst_lift and inst_split: now cterm_instantiate is used to instantiate theorems

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

isabelle