author hoelzl 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
*)
```