History log of /seL4-l4v-master/l4v/isabelle/src/HOL/Nonstandard_Analysis/HyperNat.thy
Revision Date Author Comments
# 250998b3 01-May-2019 paulson <lp15@cam.ac.uk>

De-applying and combining lemmas to make structured proofs
# 73bcc40d 30-Apr-2019 paulson <lp15@cam.ac.uk>

yet more de-applying
# ed7a971e 05-Jan-2019 wenzelm <none@none>

isabelle update -u control_cartouches;
# c7cc1919 26-Nov-2017 wenzelm <none@none>

more symbols;
# 3c65b114 31-Oct-2016 wenzelm <none@none>

tuned;
# 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