src/HOL/WF.ML
changeset 6814 d96d4977f94e
parent 6433 228237ec56e5
child 7249 4886664d7033
equal deleted inserted replaced
6813:bf90f86502b2 6814:d96d4977f94e
   234 Goalw [acyclic_def] "acyclic(r^-1) = acyclic r";
   234 Goalw [acyclic_def] "acyclic(r^-1) = acyclic r";
   235 by (simp_tac (simpset() addsimps [trancl_converse]) 1);
   235 by (simp_tac (simpset() addsimps [trancl_converse]) 1);
   236 qed "acyclic_converse";
   236 qed "acyclic_converse";
   237 
   237 
   238 Goalw [acyclic_def] "[| acyclic s; r <= s |] ==> acyclic r";
   238 Goalw [acyclic_def] "[| acyclic s; r <= s |] ==> acyclic r";
   239 by(blast_tac (claset() addIs [trancl_mono]) 1);
   239 by (blast_tac (claset() addIs [trancl_mono]) 1);
   240 qed "acyclic_subset";
   240 qed "acyclic_subset";
   241 
   241 
   242 (** cut **)
   242 (** cut **)
   243 
   243 
   244 (*This rewrite rule works upon formulae; thus it requires explicit use of
   244 (*This rewrite rule works upon formulae; thus it requires explicit use of