Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
proper theory name (cf. e84f82418e09);
authorwenzelm
Thu, 02 Dec 2010 21:23:56 +0100
changeset 40892 6f7292b94652
parent 40891 74877f1f3c68
child 40893 7d88ebdce380
child 40897 1eb1b2f9d062
proper theory name (cf. e84f82418e09);
src/HOL/Decision_Procs/Approximation.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Decision_Procs/Approximation.thy	Thu Dec 02 21:04:20 2010 +0100
+++ b/src/HOL/Decision_Procs/Approximation.thy	Thu Dec 02 21:23:56 2010 +0100
@@ -3,7 +3,7 @@
 
 header {* Prove Real Valued Inequalities by Computation *}
 
-theory Approximation_coercion
+theory Approximation
 imports Complex_Main Float Reflection "~~/src/HOL/Decision_Procs/Dense_Linear_Order" Efficient_Nat
 begin
isabelle