| #
ed7a971e |
|
05-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
| #
f62543c3 |
|
14-Aug-2018 |
paulson <lp15@cam.ac.uk> |
Zorn's lemma for relations defined by predicates
|
| #
a7ccdf43 |
|
10-Jan-2018 |
nipkow <none@none> |
ran isabelle update_op on all sources
|
| #
17bc899d |
|
18-Aug-2017 |
wenzelm <none@none> |
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
|
| #
6027fb1b |
|
31-Oct-2016 |
wenzelm <none@none> |
misc tuning and modernization;
|
| #
8c09bc20 |
|
29-Feb-2016 |
wenzelm <none@none> |
clarified session;
tuned headers;
--HG--
rename : src/HOL/NSA/CLim.thy => src/HOL/Nonstandard_Analysis/CLim.thy
rename : src/HOL/NSA/CStar.thy => src/HOL/Nonstandard_Analysis/CStar.thy
rename : src/HOL/NSA/Examples/NSPrimes.thy => src/HOL/Nonstandard_Analysis/Examples/NSPrimes.thy
rename : src/HOL/NSA/Free_Ultrafilter.thy => src/HOL/Nonstandard_Analysis/Free_Ultrafilter.thy
rename : src/HOL/NSA/HDeriv.thy => src/HOL/Nonstandard_Analysis/HDeriv.thy
rename : src/HOL/NSA/HLim.thy => src/HOL/Nonstandard_Analysis/HLim.thy
rename : src/HOL/NSA/HLog.thy => src/HOL/Nonstandard_Analysis/HLog.thy
rename : src/HOL/NSA/HSEQ.thy => src/HOL/Nonstandard_Analysis/HSEQ.thy
rename : src/HOL/NSA/HSeries.thy => src/HOL/Nonstandard_Analysis/HSeries.thy
rename : src/HOL/NSA/HTranscendental.thy => src/HOL/Nonstandard_Analysis/HTranscendental.thy
rename : src/HOL/NSA/HyperDef.thy => src/HOL/Nonstandard_Analysis/HyperDef.thy
rename : src/HOL/NSA/HyperNat.thy => src/HOL/Nonstandard_Analysis/HyperNat.thy
rename : src/HOL/NSA/Hypercomplex.thy => src/HOL/Nonstandard_Analysis/Hypercomplex.thy
rename : src/HOL/NSA/Hyperreal.thy => src/HOL/Nonstandard_Analysis/Hyperreal.thy
rename : src/HOL/NSA/NSA.thy => src/HOL/Nonstandard_Analysis/NSA.thy
rename : src/HOL/NSA/NSCA.thy => src/HOL/Nonstandard_Analysis/NSCA.thy
rename : src/HOL/NSA/NSComplex.thy => src/HOL/Nonstandard_Analysis/NSComplex.thy
rename : src/HOL/NSA/NatStar.thy => src/HOL/Nonstandard_Analysis/NatStar.thy
rename : src/HOL/NSA/Star.thy => src/HOL/Nonstandard_Analysis/Star.thy
rename : src/HOL/NSA/StarDef.thy => src/HOL/Nonstandard_Analysis/StarDef.thy
rename : src/HOL/NSA/document/root.tex => src/HOL/Nonstandard_Analysis/document/root.tex
rename : src/HOL/NSA/transfer.ML => src/HOL/Nonstandard_Analysis/transfer.ML
|