| changeset 58886 | 8a6cac7c7247 |
| parent 56073 | 29e308b56d23 |
| child 60565 | b7ee41f72add |
--- a/src/HOL/MicroJava/J/Eval.thy Sun Nov 02 17:39:52 2014 +0100 +++ b/src/HOL/MicroJava/J/Eval.thy Sun Nov 02 17:58:35 2014 +0100 @@ -3,7 +3,7 @@ Copyright 1999 Technische Universitaet Muenchen *) -header {* \isaheader{Operational Evaluation (big step) Semantics} *} +section {* Operational Evaluation (big step) Semantics *} theory Eval imports State WellType begin