# HG changeset patch
# User nipkow
# Date 1384161781 -3600
# Node ID 3fc1b77ef750121df8c9138bf49d493df15e9cac
# Parent  111ecbaa09f715e879dfa6d116bd87a2155b5a0f
tuned

diff -r 111ecbaa09f7 -r 3fc1b77ef750 src/HOL/IMP/Fold.thy
--- a/src/HOL/IMP/Fold.thy	Mon Nov 11 10:10:28 2013 +0100
+++ b/src/HOL/IMP/Fold.thy	Mon Nov 11 10:23:01 2013 +0100
@@ -1,5 +1,3 @@
-header "Constant Folding"
-
 theory Fold imports Sem_Equiv Vars begin
 
 subsection "Simple folding of arithmetic expressions"
diff -r 111ecbaa09f7 -r 3fc1b77ef750 src/HOL/IMP/Sem_Equiv.thy
--- a/src/HOL/IMP/Sem_Equiv.thy	Mon Nov 11 10:10:28 2013 +0100
+++ b/src/HOL/IMP/Sem_Equiv.thy	Mon Nov 11 10:23:01 2013 +0100
@@ -1,3 +1,5 @@
+header "Constant Folding"
+
 theory Sem_Equiv
 imports Big_Step
 begin