| #
73bcc40d |
|
30-Apr-2019 |
paulson <lp15@cam.ac.uk> |
yet more de-applying
|
| #
083015db |
|
21-Jan-2019 |
paulson <lp15@cam.ac.uk> |
new material about summations and powers, along with some tweaks
|
| #
e60cf64d |
|
06-Jan-2019 |
wenzelm <none@none> |
isabelle update -u path_cartouches;
|
| #
ed7a971e |
|
05-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
| #
cc37beb1 |
|
24-Sep-2018 |
nipkow <none@none> |
Prefix form of infix with * on either side no longer needs special treatment
because (* and *) are no longer comment brackets in terms.
|
| #
9a92542e |
|
16-Feb-2018 |
wenzelm <none@none> |
proper file name;
--HG--
rename : src/HOL/Nonstandard_Analysis/transfer.ML => src/HOL/Nonstandard_Analysis/transfer_principle.ML
|
| #
a7ccdf43 |
|
10-Jan-2018 |
nipkow <none@none> |
ran isabelle update_op on all sources
|
| #
de79d13d |
|
08-Oct-2017 |
haftmann <none@none> |
one uniform type class for parity structures
--HG--
extra : rebase_source : edf12af006cee8d114754f4a1916094166004337
|
| #
2ef94418 |
|
08-Oct-2017 |
haftmann <none@none> |
abolished (semi)ring_div in favour of euclidean_(semi)ring_cancel
--HG--
extra : rebase_source : c6612d6016d811043143eafb7a671631287494a1
|
| #
385de6ea |
|
18-Dec-2016 |
wenzelm <none@none> |
more standard notation (like infix);
|
| #
3c65b114 |
|
31-Oct-2016 |
wenzelm <none@none> |
tuned;
|
| #
6027fb1b |
|
31-Oct-2016 |
wenzelm <none@none> |
misc tuning and modernization;
|
| #
049952fc |
|
18-Oct-2016 |
haftmann <none@none> |
suitable logical type class for abs, sgn
--HG--
extra : rebase_source : 27e95dd7f038f114d0cad11ec69599a166229041
|
| #
93ff3aec |
|
17-Oct-2016 |
Simon Wimmer <wimmers@in.tum.de> |
Modified transfer principle in HOL/NSA to cause less ho-unficiation
|
| #
54a0a039 |
|
16-Oct-2016 |
haftmann <none@none> |
more standardized theorem names for facts involving the div and mod identity
|
| #
3c2b07e1 |
|
25-Sep-2016 |
haftmann <none@none> |
syntactic type class for operation mod named after mod;
simplified assumptions of type class semiring_div
--HG--
extra : rebase_source : 3714be7474835787b2a513b731c9864d1ac9d2c4
|
| #
53ecc8a7 |
|
12-Jul-2016 |
fleury <Mathias.Fleury@mpi-inf.mpg.de> |
sharing simp rules between ordered monoids and rings
|
| #
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
|