INSTALLATION OF INDUCTIVE DEFINITIONS
HOL/Sexp, List, LList: updated for inductive defs; streamlined proofs
HOL/List, Subst/UTerm, ex/Simult, ex/Term: updated refs to Sexp intr rules
HOL/Univ/diag_eqI: new
HOL/intr_elim: now checks that the inductive name does not clash with
existing theory names
HOL/Sum: now type + is an infixr, to agree with type *
HOL/Set: added Pow and the derived rules PowI, PowD, Pow_bottom, Pow_top
HOL/Fun/set_cs: now includes Pow rules
HOL/mono/Pow_mono: new
HOL/Makefile: now has Inductive.thy,.ML and ex/Acc.thy,.ML
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/Finite.thy
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
Finite powerset operator
*)
Finite = Lfp +
consts Fin :: "'a set => 'a set set"
inductive "Fin(A)"
intrs
emptyI "{} : Fin(A)"
insertI "[| a: A; b: Fin(A) |] ==> insert(a,b) : Fin(A)"
end