Thu, 19 Feb 2009 23:18:28 -0800 cleaned up
huffman [Thu, 19 Feb 2009 23:18:28 -0800] rev 30001
cleaned up
Thu, 19 Feb 2009 18:16:19 -0800 declare of_int_number_of_eq [simp]
huffman [Thu, 19 Feb 2009 18:16:19 -0800] rev 30000
declare of_int_number_of_eq [simp]
Thu, 19 Feb 2009 17:13:35 -0800 fix case_names
huffman [Thu, 19 Feb 2009 17:13:35 -0800] rev 29999
fix case_names
Thu, 19 Feb 2009 17:11:12 -0800 nicer induction/cases rules for numeral types
huffman [Thu, 19 Feb 2009 17:11:12 -0800] rev 29998
nicer induction/cases rules for numeral types
Thu, 19 Feb 2009 16:51:46 -0800 number_ring instances for numeral types
huffman [Thu, 19 Feb 2009 16:51:46 -0800] rev 29997
number_ring instances for numeral types
Thu, 19 Feb 2009 12:37:03 -0800 declare xor_compl_{left,right} [simp]
huffman [Thu, 19 Feb 2009 12:37:03 -0800] rev 29996
declare xor_compl_{left,right} [simp]
Thu, 19 Feb 2009 12:26:32 -0800 add rule for minus 1 at type bit
huffman [Thu, 19 Feb 2009 12:26:32 -0800] rev 29995
add rule for minus 1 at type bit
Thu, 19 Feb 2009 12:03:31 -0800 add formalization of a type of integers mod 2 to Library
huffman [Thu, 19 Feb 2009 12:03:31 -0800] rev 29994
add formalization of a type of integers mod 2 to Library
Thu, 19 Feb 2009 09:42:23 -0800 new theory of real inner product spaces
huffman [Thu, 19 Feb 2009 09:42:23 -0800] rev 29993
new theory of real inner product spaces
Thu, 19 Feb 2009 09:39:49 -0800 add Powerdomain_ex.thy
huffman [Thu, 19 Feb 2009 09:39:49 -0800] rev 29992
add Powerdomain_ex.thy
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip