--- a/src/HOL/ex/Commutative_Ring_Complete.thy Wed Sep 14 22:04:38 2005 +0200
+++ b/src/HOL/ex/Commutative_Ring_Complete.thy Wed Sep 14 22:08:08 2005 +0200
@@ -1,9 +1,12 @@
(* ID: $Id$
Author: Bernhard Haeupler
- This theory is about the relative completeness of the tactic
- As long as the reified atomic polynomials of type 'a pol
- are in normal form, the cring method is complete *)
+This theory is about of the relative completeness of method comm-ring
+method. As long as the reified atomic polynomials of type 'a pol are
+in normal form, the cring method is complete.
+*)
+
+header {* Proof of the relative completeness of method comm-ring *}
theory Commutative_Ring_Complete
imports Main
@@ -381,4 +384,4 @@
qed(simp)
qed
-end
\ No newline at end of file
+end