can prove the empty relation to be WF
authorpaulson
Fri, 10 Apr 1998 13:40:29 +0200
changeset 4805 20d292c05e6c
parent 4804 02b7c759159b
child 4806 79cc986bc4d7
can prove the empty relation to be WF
TFL/post.sml
--- a/TFL/post.sml	Fri Apr 10 13:15:28 1998 +0200
+++ b/TFL/post.sml	Fri Apr 10 13:40:29 1998 +0200
@@ -69,8 +69,8 @@
 *--------------------------------------------------------------------------*)
 fun std_postprocessor ss =
   Prim.postprocess
-   {WFtac      = REPEAT (ares_tac [wf_measure, wf_inv_image, wf_lex_prod, 
-				   wf_less_than, wf_trancl] 1),
+   {WFtac      = REPEAT (ares_tac [wf_empty, wf_measure, wf_inv_image, 
+				   wf_lex_prod, wf_less_than, wf_trancl] 1),
     terminator = asm_simp_tac ss 1
 		 THEN TRY(CLASET' (fn cs => best_tac
 			  (cs addSDs [not0_implies_Suc] addss ss)) 1),