tuned
authornipkow
Mon Nov 11 10:23:01 2013 +0100 (2013-11-11)
changeset 542973fc1b77ef750
parent 54296 111ecbaa09f7
child 54298 347c3b0cab44
tuned
src/HOL/IMP/Fold.thy
src/HOL/IMP/Sem_Equiv.thy
     1.1 --- a/src/HOL/IMP/Fold.thy	Mon Nov 11 10:10:28 2013 +0100
     1.2 +++ b/src/HOL/IMP/Fold.thy	Mon Nov 11 10:23:01 2013 +0100
     1.3 @@ -1,5 +1,3 @@
     1.4 -header "Constant Folding"
     1.5 -
     1.6  theory Fold imports Sem_Equiv Vars begin
     1.7  
     1.8  subsection "Simple folding of arithmetic expressions"
     2.1 --- a/src/HOL/IMP/Sem_Equiv.thy	Mon Nov 11 10:10:28 2013 +0100
     2.2 +++ b/src/HOL/IMP/Sem_Equiv.thy	Mon Nov 11 10:23:01 2013 +0100
     2.3 @@ -1,3 +1,5 @@
     2.4 +header "Constant Folding"
     2.5 +
     2.6  theory Sem_Equiv
     2.7  imports Big_Step
     2.8  begin