#
a1f8bb2d |
|
18-Sep-2019 |
paulson <lp15@cam.ac.uk> |
imported new material mostly due to Sébastien Gouëzel
|
#
250998b3 |
|
01-May-2019 |
paulson <lp15@cam.ac.uk> |
De-applying and combining lemmas to make structured proofs
|
#
ed7a971e |
|
05-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
#
47185b7e |
|
10-Jul-2018 |
paulson <lp15@cam.ac.uk> |
de-applying, etc.
|
#
d2d8a960 |
|
10-Oct-2017 |
paulson <lp15@cam.ac.uk> |
Divided Topology_Euclidean_Space in two, creating new theory Connected. Also deleted some duplicate / variant theorems
|
#
99bbcebb |
|
18-Dec-2016 |
wenzelm <none@none> |
misc tuning and modernization;
|
#
6027fb1b |
|
31-Oct-2016 |
wenzelm <none@none> |
misc tuning and modernization;
|
#
d8ffd9f3 |
|
02-Aug-2016 |
wenzelm <none@none> |
support 'abbrevs' within theory header; simplified 'keywords': no abbreviations here;
|
#
a2bc0021 |
|
25-Apr-2016 |
wenzelm <none@none> |
eliminated old 'def'; tuned comments;
|
#
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
|