Closed yutakang closed 5 years ago
The first call to the interpreter should be Eval_Syntax. And the second (= inner) call to the interpreter should be Eval_Semantics.
Eval_Syntax
Eval_Semantics
So, SeLFiE.thy should first read Eval_Semantic then Eval_Syntax.
SeLFiE.thy
Eval_Semantic
Done in e861f9ac0c21b877aa8b7f699045bc63e2601975.
The first call to the interpreter should be
Eval_Syntax
. And the second (= inner) call to the interpreter should beEval_Semantics
.So,
SeLFiE.thy
should first readEval_Semantic
thenEval_Syntax
.