Fix error in nfmbstScript.sml

HOL-Theorem-Prover · Sep 13, 2023 · 63228ef · 63228ef
1 parent 99b8c21
commit 63228ef
Showing 1 changed file with 8 additions and 8 deletions.
diff --git a/src/transfer/examples/nfmbstScript.sml b/src/transfer/examples/nfmbstScript.sml
@@ -349,14 +349,6 @@ Proof
   simp[NFMBST_def] >> metis_tac[FAPPLY_bst_to_fm]
 QED
 
-Theorem NFMfoo[transfer_rule]:
-  ((=) |==> NFMBST (=)) foo foo'
-Proof
-  simp[FUN_REL_def, foo'_def] >> gen_tac >> SELECT_ELIM_TAC >> conj_tac
-  >- metis_tac[bst_to_fm_surj] >>
-  simp[NFM_bst_to_fm]
-QED
-
 Theorem NFMEQ[transfer_rule]:
   (NFMBST (=) |==> NFMBST (=) |==> flip (==>)) (=) (=)
 Proof
@@ -374,6 +366,14 @@ Definition foo'_def:
   foo' n = @bst. bst_to_fm bst = foo n /\ wfBST bst
 End
 
+Theorem NFMfoo[transfer_rule]:
+  ((=) |==> NFMBST (=)) foo foo'
+Proof
+  simp[FUN_REL_def, foo'_def] >> gen_tac >> SELECT_ELIM_TAC >> conj_tac
+  >- metis_tac[bst_to_fm_surj] >>
+  simp[NFM_bst_to_fm]
+QED
+
 *)