nicolas.meric
/
Isabelle_DOF
forked from Isabelle_DOF/Isabelle_DOF
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Completion and a little debugging on assert*

This commit is contained in:
Burkhart Wolff 2018-12-18 17:09:24 +01:00
parent eae495ac90
commit 984915c507
1 changed files with 6 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

11
Isa_DOF.thy
View File

@ -1066,11 +1066,11 @@ fun update_instance_command (((oid:string,pos),cid_pos),
Syntax.read_term_global thy rhs)
val assns' = map conv_attrs doc_attrs
val def_trans = #1 o (calc_update_term thy cid_long assns')
val check_inv = (DOF_core.get_class_invariant cid_long thy oid {is_monitor=false})
o Context.Theory
fun check_inv thy =((DOF_core.get_class_invariant cid_long thy oid {is_monitor=false}
o Context.Theory ) thy ; thy)
in
thy |> DOF_core.update_value_global oid (def_trans)
|> (fn thy => (check_inv thy; thy))
|> check_inv
end
@ -1225,7 +1225,9 @@ val _ =
fun assert_cmd'((((((oid,pos),cid_pos),doc_attrs),some_name:string option),modes : string list),
prop:string) =
let val doc_attrs' = map (fn ((lhs,pos),rhs) => (((lhs,pos),"="),rhs)) doc_attrs
let fun markup2string x = XML.content_of (YXML.parse_body x)
val doc_attrs = (("property",pos),"[@{term ''"^markup2string prop ^"''}]")::doc_attrs
val doc_attrs' = map (fn ((lhs,pos),rhs) => (((lhs,pos),"="),rhs)) doc_attrs
(* missing : registrating t as property *)
fun mks thy = case DOF_core.get_object_global oid thy of
SOME _ => update_instance_command (((oid,pos),cid_pos),doc_attrs') thy
@ -1589,7 +1591,6 @@ val _ =
end (* struct *)
\<close>
ML\<open>find_index\<close>
section\<open> Testing and Validation \<close>