isabelle: Changelog

nipkow [Fri, 28 Jul 2000 13:04:59 +0200] rev 9457

* HOL/While

wenzelm [Thu, 27 Jul 2000 18:27:25 +0200] rev 9456

added theory While;

wenzelm [Thu, 27 Jul 2000 18:27:09 +0200] rev 9455

export has_internal; tag some rules as internal;

wenzelm [Thu, 27 Jul 2000 18:25:55 +0200] rev 9454

added thm_deps;

wenzelm [Thu, 27 Jul 2000 18:25:44 +0200] rev 9453

added enter_forward_proof;

wenzelm [Thu, 27 Jul 2000 18:25:28 +0200] rev 9452

export write_graph;

wenzelm [Thu, 27 Jul 2000 18:25:01 +0200] rev 9451

begin_theory: store *copy* of initial theory;

wenzelm [Thu, 27 Jul 2000 18:23:12 +0200] rev 9450

tuned;

wenzelm [Thu, 27 Jul 2000 11:44:29 +0200] rev 9449

intro_elim_tac: bimatch_from;

nipkow [Wed, 26 Jul 2000 19:43:28 +0200] rev 9448

While functional for defining tail-recursive functions

isabelle