replaced option_map_SomeD by option_map_eq_Some (RS iffD1)
added option_map_eq_Some to simpset(), option_map_eq_Some RS iffD1 to claset()
<HTML><HEAD><TITLE>HOL/AxClasses/README</TITLE></HEAD><BODY>
<h2>Axiomatic type classes</h2>
This directory contains the following axiomatic type class examples:
<DL>
<DT> Tutorial
<DD> Some simple axclass demos that go along with the paper <A
HREF="http://www4.informatik.tu-muenchen.de/~nipkow/isadist/axclass.dvi.gz">
"Using Axiomatic Type Classes in Isabelle --- a tutorial". </A>
<P>
<DT> Group
<DD> Some bits of group theory.
<P>
<DT> Lattice
<DD> Basic theory of lattices and orders.
</DL>
</BODY></HTML>