--- a/src/HOL/ex/Cubic_Quartic.thy Wed Jan 20 19:19:55 2016 +0100
+++ b/src/HOL/ex/Cubic_Quartic.thy Wed Jan 20 23:05:57 2016 +0100
@@ -2,7 +2,7 @@
Author: Amine Chaieb
*)
-header "The Cubic and Quartic Root Formulas"
+section "The Cubic and Quartic Root Formulas"
theory Cubic_Quartic
imports Complex_Main
--- a/src/HOL/ex/Pythagoras.thy Wed Jan 20 19:19:55 2016 +0100
+++ b/src/HOL/ex/Pythagoras.thy Wed Jan 20 23:05:57 2016 +0100
@@ -2,7 +2,7 @@
Author: Amine Chaieb
*)
-header "The Pythagorean Theorem"
+section "The Pythagorean Theorem"
theory Pythagoras
imports Complex_Main