Tue, 23 Feb 2010 14:44:43 -0800 |
huffman |
merged
|
changeset |
files
|
Tue, 23 Feb 2010 14:44:24 -0800 |
huffman |
remove redundant lemma realpow_increasing
|
changeset |
files
|
Tue, 23 Feb 2010 14:38:06 -0800 |
huffman |
remove redundant simp rules from RealPow.thy
|
changeset |
files
|
Tue, 23 Feb 2010 12:35:32 -0800 |
huffman |
adapt to new realpow rules
|
changeset |
files
|
Tue, 23 Feb 2010 11:14:09 -0800 |
huffman |
adapt to changes in simpset
|
changeset |
files
|
Tue, 23 Feb 2010 10:37:25 -0800 |
huffman |
moved some lemmas from RealPow to RealDef; changed orientation of real_of_int_power
|
changeset |
files
|
Tue, 23 Feb 2010 07:45:54 -0800 |
huffman |
move float syntax from RealPow to Rational
|
changeset |
files
|
Wed, 24 Feb 2010 11:55:52 +0100 |
blanchet |
compile
|
changeset |
files
|
Wed, 24 Feb 2010 11:35:39 +0100 |
blanchet |
merged
|
changeset |
files
|
Wed, 24 Feb 2010 11:35:10 +0100 |
blanchet |
compile
|
changeset |
files
|
Wed, 24 Feb 2010 11:07:58 +0100 |
blanchet |
make example compile
|
changeset |
files
|
Wed, 24 Feb 2010 09:59:54 +0100 |
blanchet |
got rid of "axclass", apparently
|
changeset |
files
|