src/HOL/Imperative_HOL/ex/Linked_Lists.thy
Mon, 01 Mar 2010 21:41:35 +0100 wenzelm eliminated hard tabs;
Mon, 08 Feb 2010 14:12:50 +0100 haftmann avoid upto in generated code (is infix operator in library.ML)
Thu, 10 Dec 2009 11:58:26 +0100 bulwahn added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
less more (0) tip