Quot/Examples/IntEx2.thy
Fri, 11 Dec 2009 17:19:38 +0100 Cezary Kaliszyk Renaming
Fri, 11 Dec 2009 15:58:15 +0100 Christian Urban added Int example from Larry
Fri, 11 Dec 2009 11:30:00 +0100 Cezary Kaliszyk More theorem renaming.
Fri, 11 Dec 2009 11:25:52 +0100 Cezary Kaliszyk Renamed theorems in IntEx2 to conform to names in Int.
Fri, 11 Dec 2009 11:08:58 +0100 Cezary Kaliszyk New syntax for definitions.
Thu, 10 Dec 2009 08:55:30 +0100 Cezary Kaliszyk Moved 'int_induct' to IntEx to keep IntEx2 being just theory of integers in order.
Thu, 10 Dec 2009 08:44:01 +0100 Cezary Kaliszyk Removed 'Presburger' as it introduces int & other minor cleaning in Int2.
Thu, 10 Dec 2009 03:25:42 +0100 Christian Urban merged
Thu, 10 Dec 2009 02:42:09 +0100 Cezary Kaliszyk With int_of_nat as a quotient_def, lemmas about it can be easily lifted.
Thu, 10 Dec 2009 01:48:39 +0100 Christian Urban merged
Thu, 10 Dec 2009 01:47:55 +0100 Christian Urban naming in this file cannot be made to agree to the original (PROBLEM?)
Thu, 10 Dec 2009 01:39:47 +0100 Cezary Kaliszyk Lifted some kind of induction.
Wed, 09 Dec 2009 23:32:16 +0100 Christian Urban more proofs in IntEx2
Wed, 09 Dec 2009 22:43:11 +0100 Cezary Kaliszyk Finished one proof in IntEx2.
less more (0) -14 tip