1.1 --- a/src/Tools/isac/ProgLang/Prog_Expr.thy	Thu Oct 08 10:05:33 2020 +0200
     1.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy	Thu Oct 22 14:03:40 2020 +0200
     1.3 @@ -230,6 +230,7 @@
     1.4      in SOME (thmId, HOLogic.Trueprop $ (TermC.mk_equality (t, t'))) end
     1.5    | eval_var _ _ _ _ = NONE;
     1.6  
     1.7 +(* refer to Thm.lhs_of *)
     1.8  fun lhs (Const ("HOL.eq",_) $ l $ _) = l
     1.9    | lhs t = raise ERROR("lhs called with (" ^ UnparseC.term t ^ ")");
    1.10  (*("lhs"    ,("Prog_Expr.lhs"    , eval_lhs "")):calc*)