Lines Matching refs:var
53 val ((var, body), is_forall) = (boolSyntax.dest_forall t, true)
58 (next_index + 1, (next_index, var, is_forall) :: vars, body)
93 (* 'CLAUSE_TO_SEQUENT'. Returns a list of triples ([~]i, [~]var, q), *)
138 val var = boolSyntax.dest_neg lit
140 Thm.MP (Thm.INST [{redex = var, residue = boolSyntax.F}]
150 (* ----------------- bind_var hyp var true *)
151 (* A, !var. hyp |- t *)
154 (* ----------------- bind_var hyp var false (var not free in A or t) *)
155 (* A, ?var. hyp |- t *)
158 fun bind_var thm hyp var is_forall =
161 val hyp' = boolSyntax.mk_forall (var, hyp)
162 val thm = Thm.MP (Thm.DISCH hyp thm) (Thm.SPEC var (Thm.ASSUME hyp'))
167 (* 'var' must not be free in the hypotheses of 'thm' (except in 'hyp') *)
169 val hyp' = boolSyntax.mk_exists (var, hyp)
170 val thm = Thm.CHOOSE (var, Thm.ASSUME hyp') thm
186 | forall_reduce (thm, (_, var, is_forall) :: vars, hyp, []) =
188 val (thm, hyp) = bind_var thm hyp var is_forall
192 | forall_reduce (thm, vars as (i, var, v_is_forall) :: vartail, hyp,
197 val (thm, hyp) = bind_var thm hyp var v_is_forall
211 val (thm, hyp) = bind_var thm hyp var v_is_forall