(*  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
