diff --git a/src/tests/Concept_ExampleInvariant.thy b/src/tests/Concept_ExampleInvariant.thy index 7fd00c0..a363f76 100755 --- a/src/tests/Concept_ExampleInvariant.thy +++ b/src/tests/Concept_ExampleInvariant.thy @@ -58,7 +58,7 @@ subsection*[d::A, x = "4"] \ Lorem ipsum dolor sit amet, ... \ (* test : update should not fail, invariant still valid *) update_instance*[d::A, x += "1"] -(* test : with the next step it should fail : +(* test : with the next step it should fail : update_instance*[d::A, x += "1"] *) @@ -101,19 +101,20 @@ open_monitor*[struct::M] subsection*[a::A, x = "3"] \ Lorem ipsum dolor sit amet, ... \ -text*[c1::C, x = "''beta''"] \ ... suspendisse non arcu malesuada mollis, nibh morbi, ... \ +text*[c1::C, x = "''beta''"] \ ... suspendisse non arcu malesuada mollis, nibh morbi, ... \ -text*[d1::E, a1 = "X3"] \ ... phasellus amet id massa nunc, pede suscipit repellendus, ... \ +text*[d1::E, a1 = "X3"] \ ... phasellus amet id massa nunc, pede suscipit repellendus, ... \ -text*[c2:: C, x = "''delta''"] \ ... in ut tortor eleifend augue pretium consectetuer... \ +text*[c2:: C, x = "''delta''"] \ ... in ut tortor eleifend augue pretium consectetuer... \ subsection*[f::E] \ Lectus accumsan velit ultrices, ... }\ (* -section*[f2::E] \ Lectus accumsan velit ultrices, ... }\ +section*[f2::E] \ Lectus accumsan velit ultrices, ... }\ *) -ML\val term = AttributeAccess.compute_attr_access (Context.Proof @{context}) "trace" "struct" @{here} @{here} ; +ML\val term = AttributeAccess.compute_attr_access + (Context.Proof @{context}) "trace" "struct" @{here} @{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) \