Skip to content

Commit b1e4ecf

Browse files
committed
Fix some breakage
1 parent 265cb06 commit b1e4ecf

File tree

2 files changed

+10
-0
lines changed

2 files changed

+10
-0
lines changed

icing/flover/ErrorValidationScript.sml

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,11 @@ open preambleFloVer;
1616

1717
val _ = new_theory "ErrorValidation";
1818

19+
val _ = temp_delsimps ["fromAList_def", "domain_union",
20+
"domain_inter", "domain_difference",
21+
"domain_map", "sptree.map_def", "sptree.lookup_rwts",
22+
"sptree.insert_notEmpty", "sptree.isEmpty_union"]
23+
1924
val _ = Parse.hide "delta"; (* so that it can be used as a variable *)
2025

2126
Overload abs[local] = “realax$abs”

icing/flover/IEEE_connectionScript.sml

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,11 @@ open preambleFloVer;
1313

1414
val _ = new_theory "IEEE_connection";
1515

16+
val _ = temp_delsimps ["fromAList_def", "domain_union",
17+
"domain_inter", "domain_difference",
18+
"domain_map", "sptree.map_def", "sptree.lookup_rwts",
19+
"sptree.insert_notEmpty", "sptree.isEmpty_union"]
20+
1621
Overload abs[local] = “realax$abs”
1722

1823
(** FloVer assumes rounding with ties to even, thus we exprlicitly define

0 commit comments

Comments
 (0)