diff --git a/examples/conceptual/Concept_ExampleInvariant.thy b/examples/conceptual/Concept_ExampleInvariant.thy index 67b6297a..aca91fc5 100644 --- a/examples/conceptual/Concept_ExampleInvariant.thy +++ b/examples/conceptual/Concept_ExampleInvariant.thy @@ -20,14 +20,15 @@ The implementor of an ontology must know what he does ... text\Setting a sample invariant, which simply produces some side-effect:\ setup\DOF_core.update_class_invariant "Conceptual.A" (fn oid => - fn ctxt => - (writeln ("sample echo : "^oid); true))\ + fn {is_monitor = b} => + fn ctxt => + (writeln ("sample echo : "^oid); true))\ subsection*[b::A, x = "5"] \ Lorem ipsum dolor sit amet, ... \ text\Setting a sample invariant, referring to attribute value "x":\ -ML\fun check_A_invariant oid ctxt = +ML\fun check_A_invariant oid {is_monitor:bool} ctxt = let val term = AttributeAccess.calc_attr_access ctxt "x" oid @{here} val (@{typ "int"},x_value) = HOLogic.dest_number term in if x_value > 5 then error("class A invariant violation") else true end @@ -62,7 +63,7 @@ that instances of class C occur more often as those of class D; note that this i to take sub-classing into account: \ -ML\fun check_M_invariant oid ctxt = +ML\fun check_M_invariant oid {is_monitor} ctxt = let val term = AttributeAccess.calc_attr_access ctxt "trace" oid @{here} fun conv (Const(@{const_name "Pair"},_) $ Const(s,_) $ S) = (s, HOLogic.dest_string S) val string_pair_list = map conv (HOLogic.dest_list term)