src/Pure/tactic.ML
changeset 52223 5bb6ae8acb87
parent 52087 f3075fc4f5f6
child 58837 e84d900cd287
equal deleted inserted replaced
52222:0fa3b456a267 52223:5bb6ae8acb87
   109 
   109 
   110 (** Resolution/matching tactics **)
   110 (** Resolution/matching tactics **)
   111 
   111 
   112 (*The composition rule/state: no lifting or var renaming.
   112 (*The composition rule/state: no lifting or var renaming.
   113   The arg = (bires_flg, orule, m);  see Thm.bicompose for explanation.*)
   113   The arg = (bires_flg, orule, m);  see Thm.bicompose for explanation.*)
   114 fun compose_tac arg i = PRIMSEQ (Thm.bicompose false arg i);
   114 fun compose_tac arg i =
       
   115   PRIMSEQ (Thm.bicompose {flatten = true, match = false, incremented = false} arg i);
   115 
   116 
   116 (*Converts a "destruct" rule like P&Q==>P to an "elimination" rule
   117 (*Converts a "destruct" rule like P&Q==>P to an "elimination" rule
   117   like [| P&Q; P==>R |] ==> R *)
   118   like [| P&Q; P==>R |] ==> R *)
   118 fun make_elim rl = zero_var_indexes (rl RS revcut_rl);
   119 fun make_elim rl = zero_var_indexes (rl RS revcut_rl);
   119 
   120