equal
deleted
inserted
replaced
143 |
143 |
144 * Created new image HOL-NSA, containing theories of nonstandard |
144 * Created new image HOL-NSA, containing theories of nonstandard |
145 analysis which were previously part of HOL-Complex. Entry point |
145 analysis which were previously part of HOL-Complex. Entry point |
146 Hyperreal.thy remains valid, but theories formerly using |
146 Hyperreal.thy remains valid, but theories formerly using |
147 Complex_Main.thy should now use new entry point Hypercomplex.thy. |
147 Complex_Main.thy should now use new entry point Hypercomplex.thy. |
|
148 |
|
149 |
|
150 *** ZF *** |
|
151 |
|
152 * Proof of Zorn's Lemma for partial orders. |
148 |
153 |
149 |
154 |
150 *** ML *** |
155 *** ML *** |
151 |
156 |
152 * Rules and tactics that read instantiations (read_instantiate, |
157 * Rules and tactics that read instantiations (read_instantiate, |