src/HOLCF/ex/Loop.ML
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2002-08-05 berghofe 2002-08-05 Replaced nat_ind_tac by induct_tac.
2001-11-03 wenzelm 2001-11-03 GPLed;
2001-01-09 nipkow 2001-01-09 ` -> $
2000-07-05 paulson 2000-07-05 massive tidy-up: goal -> Goal, remove use of prems, etc.
2000-06-28 paulson 2000-06-28 tidying and unbatchifying
1997-11-03 wenzelm 1997-11-03 isatool fixclasimp;
1997-10-10 wenzelm 1997-10-10 fixed dots;
1997-05-25 slotosch 1997-05-25 Eliminated the prediates flat,chfin Changed theorems with flat(x::'a) to (x::'a::flat) Since flat<chfin theorems adm_flat,adm_flatdom are eliminated. Use adm_chain_finite and adm_chfindom instead! Examples do not use flat_flat any more
1997-04-24 nipkow 1997-04-24 Updates because nat_ind_tac no longer appends "1" to the ind.var.
1997-02-17 slotosch 1997-02-17 Examples are adopted to the changes from HOLCF. Classlib is reduced. Classlib still uses arities, Classlib will change completely to new classes of ADTs
1996-12-18 oheimb 1996-12-18 removed Holcfb.thy and Holcfb.ML, moving classical3 to HOL.ML as classical2
1996-09-26 paulson 1996-09-26 Ran expandshort; used stac instead of ssubst
1996-01-30 clasohm 1996-01-30 expanded tabs
1995-10-06 regensbu 1995-10-06 added 8bit pragmas added directory ax_ops for sections axioms and ops added directory domain for sections domain and generated this is the type definition package of David Oheimb
1995-10-04 clasohm 1995-10-04 added local simpsets
1995-06-29 regensbu 1995-06-29 The curried version of HOLCF is now just called HOLCF. The old uncurried version is no longer supported
1995-04-13 regensbu 1995-04-13 adjusted HOLCF for new hyp_subst_tac
1995-02-07 clasohm 1995-02-07 added qed, qed_goal[w]
1994-01-19 nipkow 1994-01-19 HOLCF examples