equal
deleted
inserted
replaced
118 |
118 |
119 goal SubUnion.thy |
119 goal SubUnion.thy |
120 "!!u. u ~ v ==> regular(u)-->regular(v)-->regular(u un v)"; |
120 "!!u. u ~ v ==> regular(u)-->regular(v)-->regular(u un v)"; |
121 by (etac Scomp.induct 1); |
121 by (etac Scomp.induct 1); |
122 by (ALLGOALS(asm_full_simp_tac |
122 by (ALLGOALS(asm_full_simp_tac |
123 (simpset() setloop(SELECT_GOAL (safe_tac (claset())))))); |
123 (simpset() setloop(SELECT_GOAL Safe_tac)))); |
124 by (dres_inst_tac [("psi", "regular(Fun(?u) un ?v)")] asm_rl 1); |
124 by (dres_inst_tac [("psi", "regular(Fun(?u) un ?v)")] asm_rl 1); |
125 by (Asm_full_simp_tac 1); |
125 by (Asm_full_simp_tac 1); |
126 qed_spec_mp "union_preserve_regular"; |
126 qed_spec_mp "union_preserve_regular"; |