isabelle: Changelog

wenzelm [Thu, 11 Sep 1997 16:16:03 +0200] rev 3669

removed print_goals_ref (which was broken anyway);

paulson [Thu, 11 Sep 1997 12:24:28 +0200] rev 3668

Split base cases from "msg" to "atomic" in order to reduce the number of freeness theorems

paulson [Thu, 11 Sep 1997 12:22:31 +0200] rev 3667

Now uses the generic induct_tac

paulson [Thu, 11 Sep 1997 12:21:34 +0200] rev 3666

auto update

nipkow [Wed, 10 Sep 1997 14:18:12 +0200] rev 3665

Added Larry's test for preventing a datatype shadowing a theory.

nipkow [Tue, 09 Sep 1997 12:09:06 +0200] rev 3664

Example from HOLCF paper.

nipkow [Tue, 09 Sep 1997 12:08:28 +0200] rev 3663

Loads HoareEx now.

mueller [Tue, 09 Sep 1997 11:15:32 +0200] rev 3662

adm_tac extended

mueller [Tue, 09 Sep 1997 11:14:20 +0200] rev 3661

moved extended adm_tac to new place

paulson [Mon, 08 Sep 1997 10:12:28 +0200] rev 3660

added ".ML" extension in "use" command

isabelle