diff options
| author | Son Ho | 2023-09-07 16:06:14 +0200 |
|---|---|---|
| committer | Son Ho | 2023-09-07 16:06:14 +0200 |
| commit | ce8f5c8f67e41a74bfdf8f6d664ff4e45e9de850 (patch) | |
| tree | 933d2bd806026930d216e4f16f113ea2749ca250 /tests/hol4/misc-constants/constantsTheory.sig | |
| parent | 1181aecddbcb3232c21b191fbde59c2e9596846a (diff) | |
Regenerate the test files and fix a proof
Diffstat (limited to '')
| -rw-r--r-- | tests/hol4/misc-constants/constantsTheory.sig | 12 |
1 files changed, 1 insertions, 11 deletions
diff --git a/tests/hol4/misc-constants/constantsTheory.sig b/tests/hol4/misc-constants/constantsTheory.sig index 149d7e22..287ad5f5 100644 --- a/tests/hol4/misc-constants/constantsTheory.sig +++ b/tests/hol4/misc-constants/constantsTheory.sig @@ -4,8 +4,6 @@ sig (* Definitions *) val add_fwd_def : thm - val core_num_u32_max_body_def : thm - val core_num_u32_max_c_def : thm val get_z1_fwd_def : thm val get_z1_z1_body_def : thm val get_z1_z1_c_def : thm @@ -110,14 +108,6 @@ sig ⊢ ∀a b. add_fwd a b = i32_add a b - [core_num_u32_max_body_def] Definition - - ⊢ core_num_u32_max_body = Return (int_to_u32 4294967295) - - [core_num_u32_max_c_def] Definition - - ⊢ core_num_u32_max_c = get_return_value core_num_u32_max_body - [get_z1_fwd_def] Definition ⊢ get_z1_fwd = Return get_z1_z1_c @@ -321,7 +311,7 @@ sig [x1_body_def] Definition - ⊢ x1_body = Return core_num_u32_max_c + ⊢ x1_body = Return core_u32_max [x1_c_def] Definition |