Eliminated the prediates flat,chfin
Changed theorems with flat(x::'a) to (x::'a::flat)
Since flat<chfin theorems adm_flat,adm_flatdom are eliminated.
Use adm_chain_finite and adm_chfindom instead!
Examples do not use flat_flat any more
(* Title: HOLCF/porder0.thy
ID: $Id$
Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
Definition of class porder (partial order)
The prototype theory for this class is void.thy
*)
Porder0 = Void +
(* Introduction of new class. The witness is type void. *)
classes po < term
(* default type is still term ! *)
(* void is the prototype in po *)
arities void :: po
consts "<<" :: "['a,'a::po] => bool" (infixl 55)
rules
(* class axioms: justification is theory Void *)
refl_less "x << x"
(* witness refl_less_void *)
antisym_less "[|x<<y ; y<<x |] ==> x = y"
(* witness antisym_less_void *)
trans_less "[|x<<y ; y<<z |] ==> x<<z"
(* witness trans_less_void *)
(* instance of << for the prototype void *)
inst_void_po "(op <<)::[void,void]=>bool = less_void"
end