Changes

Changes from Mercurial (hg https://bitbucket.org/isa-afp/afp-devel/ default)

ZFC_in_HOL Change history
merged
Generalisation of order types to arbitrary sets; ordinal exponentiation
merged
Generalisation of the "small" predicate to arbitrary sets; Introduction of the coercion ord_of_nat :: "nat => V"; Addition of many new lemmas.

Changeset 10784:d02b36b86039 by paulson _lp15@cam.ac.uk_: ZFC_in_HOL Change history
The file was modified	`metadata/metadata`
Changeset 10783:6081d5be8d08 by paulson: merged
Changeset 10782:589397f68871 by paulson _lp15@cam.ac.uk_: Generalisation of order types to arbitrary sets; ordinal exponentiation
The file was added	`thys/ZFC_in_HOL/Ordinal_Exp.thy`
The file was modified	`metadata/metadata`
The file was modified	`thys/ZFC_in_HOL/Kirby.thy`
The file was modified	`thys/ZFC_in_HOL/ROOT`
The file was modified	`thys/ZFC_in_HOL/ZFC_Cardinals.thy`
The file was modified	`thys/ZFC_in_HOL/ZFC_in_HOL.thy`
The file was modified	`web/entries/ZFC_in_HOL.html`
The file was modified	`web/rss.xml`
The file was modified	`web/statistics.html`
Changeset 10781:85592c2f97b1 by paulson: merged
Changeset 10780:7393315c7b60 by paulson _lp15@cam.ac.uk_: Generalisation of the "small" predicate to arbitrary sets;<br> Introduction of the coercion ord_of_nat :: "nat => V";<br> Addition of many new lemmas.
The file was modified	`metadata/metadata`
The file was modified	`thys/ZFC_in_HOL/Kirby.thy`
The file was modified	`thys/ZFC_in_HOL/ZFC_Cardinals.thy`
The file was modified	`thys/ZFC_in_HOL/ZFC_Typeclasses.thy`
The file was modified	`thys/ZFC_in_HOL/ZFC_in_HOL.thy`