src/HOL/IMP/ROOT.ML
2010-03-12 nipkow 2010-03-12 Reorganized Hoare logic theories; added Hoare_Den
2010-03-12 nipkow 2010-03-12 Added Hoare_Op.thy
2008-10-14 nipkow 2008-10-14 Added liveness analysis
2007-07-31 wenzelm 2007-07-31 simultaneous use_thys;
2002-04-26 nipkow 2002-04-26 New machine architecture and other direction of compiler proof.
2000-10-26 nipkow 2000-10-26 *** empty log message ***
2000-07-07 oheimb 2000-07-07 added dependency caveat
2000-07-07 oheimb 2000-07-07 added dependency caveat
2000-07-04 oheimb 2000-07-04 disambiguated := ; added Examples (factorial)
2000-05-30 wenzelm 2000-05-30 cleaned up;
1999-03-11 wenzelm 1999-03-11 removed foo_build_completed -- now handled by session management (via usedir);
1997-12-19 wenzelm 1997-12-19 tuned;
1996-04-27 nipkow 1996-04-27 A completely new version of IMP.
1996-01-30 clasohm 1996-01-30 expanded tabs
1996-01-23 nipkow 1996-01-23 Added a verified verification-condition generator.
1995-11-21 clasohm 1995-11-21 removed make_chart; theories are now read from the current directory (because of use_dir)
1995-11-17 nipkow 1995-11-17 *** empty log message ***
1995-10-24 clasohm 1995-10-24 added calls of init_html and make_chart
1995-06-29 clasohm 1995-06-29 renamed CHOL to HOL
1995-04-10 nipkow 1995-04-10 Removed the "exit 1" calls, since now the Makefile does them.
1995-03-14 nipkow 1995-03-14 added exit 1
1995-03-07 nipkow 1995-03-07 Hoare logic
1995-03-03 clasohm 1995-03-03 new version of HOL/IMP with curried function application