src/HOLCF/Fix.ML
changeset 300 3fb8c0256bec
parent 297 5ef75ff3baeb
child 430 89e1986125fe
equal deleted inserted replaced
299:febeb36a4ba4 300:3fb8c0256bec
   892 	(res_inst_tac [("s","False"),("t","Suc(ia) < Suc(i)")] ssubst 1),
   892 	(res_inst_tac [("s","False"),("t","Suc(ia) < Suc(i)")] ssubst 1),
   893 	(asm_simp_tac nat_ss  1),
   893 	(asm_simp_tac nat_ss  1),
   894 	(rtac iffI 1),
   894 	(rtac iffI 1),
   895 	(etac FalseE 2),
   895 	(etac FalseE 2),
   896 	(rtac notE 1),
   896 	(rtac notE 1),
   897 	(etac (less_not_sym RS mp) 1),	
   897 	(etac less_not_sym 1),	
   898 	(atac 1),
   898 	(atac 1),
   899 	(asm_simp_tac Cfun_ss  1),
   899 	(asm_simp_tac Cfun_ss  1),
   900 	(etac (is_chainE RS spec) 1),
   900 	(etac (is_chainE RS spec) 1),
   901 	(hyp_subst_tac 1),
   901 	(hyp_subst_tac 1),
   902 	(asm_simp_tac nat_ss 1),
   902 	(asm_simp_tac nat_ss 1),
   932 		ssubst 1),
   932 		ssubst 1),
   933 	(res_inst_tac [("s","False"),("t","n < Suc(i)")] ssubst 1),
   933 	(res_inst_tac [("s","False"),("t","n < Suc(i)")] ssubst 1),
   934 	(rtac iffI 1),
   934 	(rtac iffI 1),
   935 	(etac FalseE 2),
   935 	(etac FalseE 2),
   936 	(rtac notE 1),
   936 	(rtac notE 1),
   937 	(etac (less_not_sym RS mp) 1),	
   937 	(etac less_not_sym 1),	
   938 	(atac 1),
   938 	(atac 1),
   939 	(asm_simp_tac nat_ss 1),
   939 	(asm_simp_tac nat_ss 1),
   940 	(dtac spec 1),
   940 	(dtac spec 1),
   941 	(rtac mp 1),
   941 	(rtac mp 1),
   942 	(atac 1),
   942 	(atac 1),