INSTALLATION OF INDUCTIVE DEFINITIONS
HOL/ex/MT.thy: now mentions dependence upon Sum.thy
HOL/ex/Acc: new example, borrowed & adapted from ZF
HOL/ex/Simult, ex/Term: updated refs to Sexp intr rules
HOL/Sexp,List,LList,ex/Term: converted as follows
node *set -> item
Sexp -> sexp
LList_corec -> <self>
LList_ -> llist_
LList\> -> llist
List_case -> <self>
List_rec -> <self>
List_ -> list_
List\> -> list
Term_rec -> <self>
Term_ -> term_
Term\> -> term
(* Title: HOL/Ord.thy
ID: $Id$
Author: Tobias Nipkow, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
The type class for ordered types
*)
Ord = HOL +
classes
ord < term
consts
"<", "<=" :: "['a::ord, 'a] => bool" (infixl 50)
mono :: "['a::ord => 'b::ord] => bool" (*monotonicity*)
min,max :: "['a::ord,'a] => 'a"
rules
mono_def "mono(f) == (!A B. A <= B --> f(A) <= f(B))"
min_def "min(a,b) == if(a <= b, a, b)"
max_def "max(a,b) == if(a <= b, b, a)"
end