author | berghofe |
Fri, 21 Jun 1996 13:39:08 +0200 | |
changeset 1822 | c192d7dc22e7 |
parent 1821 | bc506bcb9fe4 |
child 1823 | e1458e1a9f80 |
src/HOL/Fun.ML | file | annotate | diff | comparison | revisions |
--- a/src/HOL/Fun.ML Fri Jun 21 13:34:55 1996 +0200 +++ b/src/HOL/Fun.ML Fri Jun 21 13:39:08 1996 +0200 @@ -189,4 +189,4 @@ addEs [ballE, InterD, InterE, INT_D, INT_E, make_elim INT1_D, subsetD, subsetCE]; -fun cfast_tac prems = cut_facts_tac prems THEN' fast_tac set_cs; +fun cfast_tac prems = cut_facts_tac prems THEN' fast_tac (claset_of "Fun");