src/ZF/Perm.ML
changeset 2688 889a1cbd1aca
parent 2637 e9b203f854ae
child 3016 15763781afb0
     1.1 --- a/src/ZF/Perm.ML	Fri Feb 28 15:44:32 1997 +0100
     1.2 +++ b/src/ZF/Perm.ML	Fri Feb 28 15:46:41 1997 +0100
     1.3 @@ -238,10 +238,10 @@
     1.4  by (REPEAT (eresolve_tac [CollectE, exE, conjE] 1 ORELSE ares_tac prems 1));
     1.5  qed "compE";
     1.6  
     1.7 -val compEpair = 
     1.8 +bind_thm ("compEpair", 
     1.9      rule_by_tactic (REPEAT_FIRST (etac Pair_inject ORELSE' bound_hyp_subst_tac)
    1.10                      THEN prune_params_tac)
    1.11 -        (read_instantiate [("xz","<a,c>")] compE);
    1.12 +        (read_instantiate [("xz","<a,c>")] compE));
    1.13  
    1.14  AddSIs [idI];
    1.15  AddIs  [compI];