domain package:
* theorems are stored in the theory
* creates hierachical name space
* minor changes to some names and values (for consistency),
e.g. cases -> casedist, dists_eq -> dist_eqs,
[take_lemma] -> take_lemmas
* separator between mutual domain definitions changed from "," to "and"
* minor debugging of Domain_Library.mk_var_names
(* Title: HOLCF/Porder0.thy
ID: $Id$
Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
Definition of class porder (partial order)
*)
Porder0 = Arith +
(* introduce a (syntactic) class for the constant << *)
axclass sq_ord<term
(* characteristic constant << for po *)
consts
"<<" :: "['a,'a::sq_ord] => bool" (infixl 55)
syntax (symbols)
"op <<" :: "['a,'a::sq_ord] => bool" (infixl "\\<sqsubseteq>" 55)
axclass po < sq_ord
(* class axioms: *)
refl_less "x << x"
antisym_less "[|x << y; y << x |] ==> x = y"
trans_less "[|x << y; y << z |] ==> x << z"
end