src/HOLCF/ex/Loop.ML
Mon, 21 Jun 2004 10:25:57 +0200 kleing Merged in license change from Isabelle2004
Mon, 05 Aug 2002 14:32:56 +0200 berghofe Replaced nat_ind_tac by induct_tac.
Sat, 03 Nov 2001 18:41:28 +0100 wenzelm GPLed;
Tue, 09 Jan 2001 15:36:30 +0100 nipkow ` -> $
Wed, 05 Jul 2000 16:37:52 +0200 paulson massive tidy-up: goal -> Goal, remove use of prems, etc.
Wed, 28 Jun 2000 10:54:21 +0200 paulson tidying and unbatchifying
Mon, 03 Nov 1997 14:06:27 +0100 wenzelm isatool fixclasimp;
Fri, 10 Oct 1997 19:02:28 +0200 wenzelm fixed dots;
Sun, 25 May 1997 16:17:09 +0200 slotosch Eliminated the prediates flat,chfin
Thu, 24 Apr 1997 18:51:14 +0200 nipkow Updates because nat_ind_tac no longer appends "1" to the ind.var.
Mon, 17 Feb 1997 11:04:00 +0100 slotosch Examples are adopted to the changes from HOLCF.
Wed, 18 Dec 1996 15:16:13 +0100 oheimb removed Holcfb.thy and Holcfb.ML, moving classical3 to HOL.ML as classical2
Thu, 26 Sep 1996 15:14:23 +0200 paulson Ran expandshort; used stac instead of ssubst
Tue, 30 Jan 1996 13:42:57 +0100 clasohm expanded tabs
Fri, 06 Oct 1995 17:25:24 +0100 regensbu added 8bit pragmas
Wed, 04 Oct 1995 14:01:44 +0100 clasohm added local simpsets
Thu, 29 Jun 1995 16:28:40 +0200 regensbu The curried version of HOLCF is now just called HOLCF. The old
Thu, 13 Apr 1995 14:25:45 +0200 regensbu adjusted HOLCF for new hyp_subst_tac
Tue, 07 Feb 1995 11:59:32 +0100 clasohm added qed, qed_goal[w]
Wed, 19 Jan 1994 17:40:26 +0100 nipkow HOLCF examples
less more (0) tip