diff --git a/src/ontologies/Conceptual/Conceptual.thy b/src/ontologies/Conceptual/Conceptual.thy index 0ae6409..ae32da3 100755 --- a/src/ontologies/Conceptual/Conceptual.thy +++ b/src/ontologies/Conceptual/Conceptual.thy @@ -167,6 +167,7 @@ ML\ Thy_Header.get_keywords @{theory};(* this looks to be really theory gl open_monitor*[aaa::M] section*[test::A]\Test and Validation\ +term\Conceptual.M.make\ text\Defining some document elements to be referenced in later on in another theory: \ text*[sdf]\ Lorem ipsum @{thm refl}\ text*[ sdfg :: F] \ Lorem ipsum @{thm refl}\ diff --git a/src/tests/Attributes.thy b/src/tests/Attributes.thy index fd6aaa3..df09354 100755 --- a/src/tests/Attributes.thy +++ b/src/tests/Attributes.thy @@ -45,6 +45,7 @@ value "tag_attribute(M.make undefined_AAA [] ())" value "ok(M.make 0 [] ())" (* +value "ok(M.make undefined [] ())" value "ok(M.make 0 [] undefined)" *) @@ -55,6 +56,14 @@ value [simp] \ M.ok (undefined::M)) ))\ +value \ M.ok + (Conceptual.M.trace_update (\x. []) + (Conceptual.M.tag_attribute_update (\x. 0) + (Conceptual.M.ok_update (\x. ()) + (M.make XX1 XX2 XX3::M)) + ))\ + + ML\ fun fac x = if x = 0 then 1 else x * (fac(x -1));