We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 8c9c4fc commit eb0e706Copy full SHA for eb0e706
2 files changed
hol/polygram/README.md
@@ -108,7 +108,10 @@ type the following:
108
109
110
111
- For checking MTBDD only (Table I)
+ For checking MTBDD only (Table I) bdd_test_cases have three theorems
112
+ policy_trans_fwd
113
+ policy_trans_fwd_proof
114
+ policy_BDD
115
116
117
to exit holmode:
hol/polygram/bdd_policy_cakeLib.sig
@@ -1,9 +1,9 @@
1
-signature fwd_proof_cakeLib =
+signature bdd_policy_cakeLib =
2
sig
3
include Abbrev
4
5
6
- val convert_arith_policy_to_interval_tables_cake : term * term * term * term * term * string -> thm
+ val convert_arith_policy_to_bdd : term * term * term * term * term * string -> thm
7
8
9
end
0 commit comments