src/HOL/Nonstandard_Analysis/StarDef.thy
Tue, 30 Apr 2019 17:03:32 +0100 paulson yet more de-applying
Mon, 21 Jan 2019 14:44:23 +0000 paulson new material about summations and powers, along with some tweaks
Sun, 06 Jan 2019 15:04:34 +0100 wenzelm isabelle update -u path_cartouches;
Sat, 05 Jan 2019 17:24:33 +0100 wenzelm isabelle update -u control_cartouches;
Mon, 24 Sep 2018 14:30:09 +0200 nipkow Prefix form of infix with * on either side no longer needs special treatment
Fri, 16 Feb 2018 21:40:15 +0100 wenzelm proper file name;
Wed, 10 Jan 2018 15:25:09 +0100 nipkow ran isabelle update_op on all sources
Sun, 08 Oct 2017 22:28:22 +0200 haftmann one uniform type class for parity structures
Sun, 08 Oct 2017 22:28:21 +0200 haftmann abolished (semi)ring_div in favour of euclidean_(semi)ring_cancel
Sun, 18 Dec 2016 16:13:20 +0100 wenzelm more standard notation (like infix);
Tue, 01 Nov 2016 01:04:53 +0100 wenzelm tuned;
Tue, 01 Nov 2016 00:44:24 +0100 wenzelm misc tuning and modernization;
Tue, 18 Oct 2016 18:48:53 +0200 haftmann suitable logical type class for abs, sgn
Mon, 17 Oct 2016 15:23:06 +0200 Simon Wimmer Modified transfer principle in HOL/NSA to cause less ho-unficiation
Sun, 16 Oct 2016 09:31:05 +0200 haftmann more standardized theorem names for facts involving the div and mod identity
Mon, 26 Sep 2016 07:56:54 +0200 haftmann syntactic type class for operation mod named after mod;
Tue, 12 Jul 2016 13:55:35 +0200 fleury sharing simp rules between ordered monoids and rings
Mon, 29 Feb 2016 22:34:36 +0100 wenzelm clarified session;
less more (0) tip