src/HOL/UNITY/Constrains.ML
changeset 6741 540fc00ec32b
parent 6739 66e4118eead9
child 7403 c318acb88251
equal deleted inserted replaced
6740:5b5bf511fdd5 6741:540fc00ec32b
   347 	      rtac constrainsI 1,
   347 	      rtac constrainsI 1,
   348 	      Full_simp_tac 1,
   348 	      Full_simp_tac 1,
   349 	      REPEAT (FIRSTGOAL (etac disjE)),
   349 	      REPEAT (FIRSTGOAL (etac disjE)),
   350 	      ALLGOALS Clarify_tac,
   350 	      ALLGOALS Clarify_tac,
   351 	      ALLGOALS Asm_full_simp_tac]) i;
   351 	      ALLGOALS Asm_full_simp_tac]) i;
   352 
       
   353 
       
   354 leadsTo_wf_induct