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.
Updated paths in Decision_Procs comments and NEWS
authorhoelzl
Wed, 11 Mar 2009 10:58:18 +0100
changeset 30439 57c68b3af2ea
parent 30432 aad3cd70e25a
child 30441 193cf2fa692a
child 30446 e3641cac56fa
Updated paths in Decision_Procs comments and NEWS
NEWS file | annotate | diff | comparison | revisions
src/HOL/Decision_Procs/Approximation.thy file | annotate | diff | comparison | revisions
src/HOL/Decision_Procs/Cooper.thy file | annotate | diff | comparison | revisions
src/HOL/Decision_Procs/Dense_Linear_Order.thy file | annotate | diff | comparison | revisions
src/HOL/Decision_Procs/Ferrack.thy file | annotate | diff | comparison | revisions
src/HOL/Decision_Procs/MIR.thy file | annotate | diff | comparison | revisions
src/HOL/Decision_Procs/cooper_tac.ML file | annotate | diff | comparison | revisions
src/HOL/Decision_Procs/ferrack_tac.ML file | annotate | diff | comparison | revisions
src/HOL/Decision_Procs/mir_tac.ML file | annotate | diff | comparison | revisions 
--- a/NEWS	Wed Mar 11 08:45:57 2009 +0100
+++ b/NEWS	Wed Mar 11 10:58:18 2009 +0100
@@ -244,7 +244,8 @@
 * Theory HOL/Decisioin_Procs/Approximation.thy provides the new proof method
 "approximation".  It proves formulas on real values by using interval arithmetic.
 In the formulas are also the transcendental functions sin, cos, tan, atan, ln,
-exp and the constant pi are allowed.  For examples see HOL/ex/ApproximationEx.thy.
+exp and the constant pi are allowed. For examples see
+HOL/Descision_Procs/ex/Approximation_Ex.thy.
 
 * Theory "Reflection" now resides in HOL/Library.
 
--- a/src/HOL/Decision_Procs/Approximation.thy	Wed Mar 11 08:45:57 2009 +0100
+++ b/src/HOL/Decision_Procs/Approximation.thy	Wed Mar 11 10:58:18 2009 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Reflection/Approximation.thy
+(*  Title:      HOL/Decision_Procs/Approximation.thy
     Author:     Johannes Hoelzl <hoelzl@in.tum.de> 2008 / 2009
 *)
 
--- a/src/HOL/Decision_Procs/Cooper.thy	Wed Mar 11 08:45:57 2009 +0100
+++ b/src/HOL/Decision_Procs/Cooper.thy	Wed Mar 11 10:58:18 2009 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Reflection/Cooper.thy
+(*  Title:      HOL/Decision_Procs/Cooper.thy
     Author:     Amine Chaieb
 *)
 
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Wed Mar 11 08:45:57 2009 +0100
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Wed Mar 11 10:58:18 2009 +0100
@@ -1,4 +1,4 @@
-(*  Title       : HOL/Dense_Linear_Order.thy
+(*  Title       : HOL/Decision_Procs/Dense_Linear_Order.thy
     Author      : Amine Chaieb, TU Muenchen
 *)
 
--- a/src/HOL/Decision_Procs/Ferrack.thy	Wed Mar 11 08:45:57 2009 +0100
+++ b/src/HOL/Decision_Procs/Ferrack.thy	Wed Mar 11 10:58:18 2009 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Reflection/Ferrack.thy
+(*  Title:      HOL/Decision_Procs/Ferrack.thy
     Author:     Amine Chaieb
 *)
 
--- a/src/HOL/Decision_Procs/MIR.thy	Wed Mar 11 08:45:57 2009 +0100
+++ b/src/HOL/Decision_Procs/MIR.thy	Wed Mar 11 10:58:18 2009 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Reflection/MIR.thy
+(*  Title:      HOL/Decision_Procs/MIR.thy
     Author:     Amine Chaieb
 *)
 
--- a/src/HOL/Decision_Procs/cooper_tac.ML	Wed Mar 11 08:45:57 2009 +0100
+++ b/src/HOL/Decision_Procs/cooper_tac.ML	Wed Mar 11 10:58:18 2009 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Reflection/cooper_tac.ML
+(*  Title:      HOL/Decision_Procs/cooper_tac.ML
     Author:     Amine Chaieb, TU Muenchen
 *)
 
--- a/src/HOL/Decision_Procs/ferrack_tac.ML	Wed Mar 11 08:45:57 2009 +0100
+++ b/src/HOL/Decision_Procs/ferrack_tac.ML	Wed Mar 11 10:58:18 2009 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Reflection/ferrack_tac.ML
+(*  Title:      HOL/Decision_Procs/ferrack_tac.ML
     Author:     Amine Chaieb, TU Muenchen
 *)
 
--- a/src/HOL/Decision_Procs/mir_tac.ML	Wed Mar 11 08:45:57 2009 +0100
+++ b/src/HOL/Decision_Procs/mir_tac.ML	Wed Mar 11 10:58:18 2009 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Reflection/mir_tac.ML
+(*  Title:      HOL/Decision_Procs/mir_tac.ML
     Author:     Amine Chaieb, TU Muenchen
 *)
isabelle