Searched refs:newVar (Results 1 - 12 of 12) sorted by relevance

/seL4-l4v-10.1.1/HOL4/src/HolSat/sat_solvers/minisat/
H A DVarOrder.h47 inline void newVar(void);
54 void VarOrder::newVar(void) function in class:VarOrder
H A DSolver.h180 Var newVar ();
H A DMain.C34 while (var >= S.nVars()) S.newVar();
H A DSolver.C189 Var Solver::newVar() {
200 order .newVar();
/seL4-l4v-10.1.1/HOL4/examples/temporal_deep/src/tools/
H A Dtuerk_tacticsLib.sml16 val newVar = variant (free_varsl (t::asl)) lvar value
17 val newLBody = subst[lvar |-> newVar] LBody
18 val newRBody = subst[rvar |-> newVar] RBody
21 fn thList => EXISTS_EQ newVar (hd(thList)))
31 val newVar = variant (free_varsl (t::asl)) lvar value
32 val newLBody = subst[lvar |-> newVar] LBody
33 val newRBody = subst[rvar |-> newVar] RBody
36 fn thList => FORALL_EQ newVar (hd thList))
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/
H A DTerm.sig117 val newVar : unit -> term value
H A DSubst.sml155 fun add (v,m) = insert m (v, Term.newVar ())
H A DTerm.sml236 fun newVar () = Var (Name.newName ()); function
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/
H A DTerm.sig117 val newVar : unit -> term value
H A DSubst.sml155 fun add (v,m) = insert m (v, Term.newVar ())
H A DTerm.sml236 fun newVar () = Var (Name.newName ()); function
/seL4-l4v-10.1.1/HOL4/examples/elliptic/swsep/
H A DswsepScript.sml63 val newVar = variant (free_varsl (t::asl)) lvar value
64 val newLBody = subst[lvar |-> newVar] LBody
65 val newRBody = subst[rvar |-> newVar] RBody
68 fn thList => FORALL_EQ newVar (hd thList))

Completed in 116 milliseconds