| Wed, 11 Jul 2007 11:14:51 +0200 | berghofe | Adapted to new inductive definition package. | file | diff | annotate |
| Fri, 17 Nov 2006 02:20:03 +0100 | wenzelm | more robust syntax for definition/abbreviation/notation; | file | diff | annotate |
| Thu, 28 Sep 2006 23:42:35 +0200 | wenzelm | replaced syntax/translations by abbreviation; | file | diff | annotate |
| Fri, 10 Mar 2006 15:33:48 +0100 | haftmann | renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc. | file | diff | annotate |
| Tue, 16 Aug 2005 19:25:42 +0200 | nipkow | name fix | file | diff | annotate |
| Fri, 17 Jun 2005 16:12:49 +0200 | haftmann | migrated theory headers to new format | file | diff | annotate |
| Mon, 11 Oct 2004 07:42:22 +0200 | nipkow | Proofs needed to be updated because induction now preserves name of | file | diff | annotate |
| Sun, 21 Dec 2003 18:39:27 +0100 | paulson | tidying of HOL/Auth esp Guard lemmas | file | diff | annotate |
| Wed, 21 Aug 2002 15:53:30 +0200 | paulson | Frederic Blanqui's new "guard" examples | file | diff | annotate |