src/HOL/AxClasses/Group/Sigs.thy
author clasohm
Wed, 20 Mar 1996 13:21:12 +0100
changeset 1589 fd6a571cb2b0
parent 1247 18b1441fb603
child 2907 0e272e4c7cb2
permissions -rw-r--r--
added warning and automatic deactivation of HTML generation if we cannot write .theory_list.txt; fixed bug which occured when index_path's value is "/"

(*  Title:      Sigs.thy
    ID:         $Id$
    Author:     Markus Wenzel, TU Muenchen
*)

Sigs = HOL +

axclass
  inv < term

axclass
  one < term

consts
  "inv" :: "'a::inv => 'a"
  "1"   :: "'a::one"                    ("1")

end