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