src/HOL/Hyperreal/HyperNat.thy
Wed, 20 Jun 2007 05:18:39 +0200 huffman change simp rules for of_nat to work like int did previously (reorient of_nat_Suc, remove of_nat_mult [simp]); preserve original variable names in legacy int theorems
Sat, 16 Dec 2006 20:23:45 +0100 huffman moved several theorems; rearranged theory dependencies
Sat, 16 Dec 2006 19:37:07 +0100 huffman hypreal_of_hypnat abbreviates more general of_hypnat
Thu, 14 Dec 2006 22:09:26 +0100 huffman remove ultra tactic and redundant FreeUltrafilterNat lemmas
Thu, 14 Dec 2006 18:10:38 +0100 huffman redefine hSuc as *f* Suc, and move to HyperNat.thy
Tue, 12 Dec 2006 07:46:40 +0100 huffman consistent naming for FreeUltrafilterNat lemmas; cleaned up
Fri, 17 Nov 2006 02:20:03 +0100 wenzelm more robust syntax for definition/abbreviation/notation;
Wed, 27 Sep 2006 21:44:38 +0200 huffman reorganized HNatInfinite proofs; simplified and renamed some lemmas
Wed, 27 Sep 2006 07:09:19 +0200 huffman hypreal_of_nat abbreviates of_nat
Sun, 24 Sep 2006 07:18:16 +0200 huffman moved SEQ_Infinitesimal from SEQ to HyperNat
Sat, 16 Sep 2006 02:40:00 +0200 huffman generalized types of many constants to work over arbitrary vector spaces;
Fri, 02 Jun 2006 23:22:29 +0200 wenzelm misc cleanup;
Sun, 09 Apr 2006 18:51:13 +0200 wenzelm tuned syntax/abbreviations;
Fri, 16 Sep 2005 02:20:50 +0200 huffman rearranged
Thu, 15 Sep 2005 23:46:22 +0200 huffman merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
Mon, 12 Sep 2005 23:14:41 +0200 huffman added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
Fri, 09 Sep 2005 19:34:22 +0200 huffman starfun, starset, and other functions on NS types are now polymorphic;
Wed, 07 Sep 2005 00:48:50 +0200 huffman replace type hypnat with nat star
Tue, 06 Sep 2005 23:16:48 +0200 huffman replace type hypreal with real star
Wed, 15 Dec 2004 17:32:40 +0100 paulson removal of archaic Abs/Rep proofs
Tue, 19 Oct 2004 18:18:45 +0200 paulson converted some induct_tac to induct
Wed, 01 Sep 2004 15:04:01 +0200 paulson new "respects" syntax for quotienting
Wed, 18 Aug 2004 11:09:40 +0200 nipkow import -> imports
Mon, 16 Aug 2004 14:22:27 +0200 nipkow New theory header syntax.
Wed, 21 Jul 2004 08:35:29 +0200 nipkow Fixed latex problem
Fri, 16 Jul 2004 17:31:44 +0200 nipkow Corrected TeX problems.
Tue, 11 May 2004 20:11:08 +0200 obua changes made due to new Ring_and_Field theory
Sat, 01 May 2004 22:01:57 +0200 wenzelm tuned instance statements;
Fri, 23 Apr 2004 11:04:07 +0200 paulson congruent2 now allows different equiv relations
Mon, 15 Mar 2004 10:46:19 +0100 paulson heavy tidying
less more (0) -30 tip