pierre.derathe
/
Isabelle_DOF
Archived
forked from Isabelle_DOF/Isabelle_DOF
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Handle normalization of trace attribute

This commit is contained in:
Nicolas Méric 2022-05-26 12:56:21 +02:00
parent 9981c31966
commit 83c790d66a
1 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
src/DOF/Isa_DOF.thy
View File

@ -1406,8 +1406,8 @@ fun register_oid_cid_in_open_monitors oid pos cid_long thy =
fun def_trans_input_term oid =
#1 o (calc_update_term {mk_elaboration=false} thy (cid_of oid) assns')
fun def_trans_value oid =
#1 o (calc_update_term {mk_elaboration=true} thy (cid_of oid) assns')
(#1 o (calc_update_term {mk_elaboration=true} thy (cid_of oid) assns'))
#> value (Proof_Context.init_global thy)
val _ = if null enabled_monitors then () else writeln "registrating in monitors ..."
val _ = app (fn n => writeln(oid^" : "^cid_long^" ==> "^n)) enabled_monitors;
(* check that any transition is possible : *)