(* Title: HOL/ex/AVL.thy ID: $Id: AVL_fragment1.thy,v 1.7 2008/02/11 15:29:14 smaus Exp $ Author: Cornelia Pusch and Tobias Nipkow modified by B. Wolff Copyright 1998 TUM AVL trees: at the moment only insertion. This version works exclusively with nat. This is a fragment for the AVL.thy file as received by Smaus from Wolff. It is part of exercise sheet 13. *) AVL = Main + datatype 'a tree = Leaf | Node 'a ('a tree) ('a tree) consts height :: "'a tree => nat" isin :: isord :: primrec "height Leaf = 0" "height (Node n l r) = Suc(max (height l) (height r))" end