HOL-OCL
/
su4sml
1
0
Fork 0
Code Issues Pull Requests Releases Activity

holOclLib.forall -> holOclLib.forAll 

git-svn-id: https://projects.brucker.ch/su4sml/svn/su4sml/trunk@7940 3260e6d1-4efc-4170-b0a7-36055960796d
This commit is contained in:
Manuel Krucker 2008-05-10 09:16:18 +00:00
parent 8e8a95c260
commit 90adbedab6
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
su4sml/src/wfcpog/operational_consistency.sml
View File

@ -79,7 +79,7 @@ fun impl_op_operation class oper =
val impl = OperationCall (pre_of_op,Boolean,["holOclLib","Boolean","implies"],[(lv_post,Boolean)],Boolean)
val lv_state = OperationCall(impl,Boolean,["holOclLib","Boolean","OclLocalValid"],[(tuple_term,OclState)],Boolean)
val holocl_exists = Iterator("holOclLib.exists",[("sigma_s",OclState)],Literal("",DummyT),DummyT,lv_state,Boolean,Boolean)
val holocl_forall = Iterator("holOclLib.forall",[("sigma",OclState)],Literal("",DummyT),DummyT,holocl_exists,Boolean,Boolean)
val holocl_forall = Iterator("holOclLib.forAll",[("sigma",OclState)],Literal("",DummyT),DummyT,holocl_exists,Boolean,Boolean)
val _ = trace function_ends ("WFCPOG_Operational_Consistency.prestate_complete_operaiton\n")
in
holocl_forall