Commit 92854d7c authored by Heiko Becker's avatar Heiko Becker

Fix IEEE_connection Script

parent 5f55f541
......@@ -1342,9 +1342,6 @@ val getValidMap_preserving = store_thm (
\\ strip_tac \\ rveq \\ fs[map_find_add]
\\ Cases_on `e' = Downcast M64 e` \\ fs[] \\ rveq
\\ res_tac);
>- (Cases_on `m = M64` \\ fs[]
>- (Cases_on `FloverMapTree_find (Downcast m e) defVars` \\ fs[]
>- (fs[isMonotone_def]
val getValidMapCmd_preserving = store_thm (
"getValidMapCmd_preserving",
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment