/seL4-l4v-10.1.1/HOL4/examples/hardware/hol88/mos-count/ |
H A D | toplevel.ml | 68 else let var = fst (dest_forall (concl thm)) in 69 if not (type_of tm = type_of var) then ALL_TAC
|
/seL4-l4v-10.1.1/HOL4/examples/muddy/muddyC/buddy/src/ |
H A D | cppext.cxx | 98 BDD *var = NEW(BDD,width); local 104 var[n] = variables[n].root; 106 res = bdd_buildcube(val, width, var); 108 free(var); 186 void printhandler(ostream &o, int var) 189 o << names[var]; 510 void printhandler(ostream &o, int var) 513 o << names[var];
|
/seL4-l4v-10.1.1/HOL4/src/quotient/examples/lambda/ |
H A D | variableScript.sml | 58 val _ = Hol_datatype `var = VAR of string => num`; 91 (* RW_TAC std_ss (type_rws "var") (* or list_ss or arith_ss *) *) 171 new_infix("is_variant", ==`:var->var->bool`==, 450); 464 ���SUC(CARD (s:var -> bool))���] LESS_CASES) 535 THEN ASSUME_TAC (INST_TYPE[==`:'a`== |-> ==`:var`==] FINITE_EMPTY) 578 THEN EXISTS_TAC ���s:var -> bool��� 681 THEN IMP_RES_THEN (ASSUME_TAC o SPEC ���x:var���) variant_THM 739 THEN EXISTS_TAC ���(y:var) INSERT s��� 843 THEN (MP_TAC o SPECL[���x:(var)lis [all...] |
/seL4-l4v-10.1.1/HOL4/src/quotient/examples/sigma/ |
H A D | variableScript.sml | 64 val _ = Hol_datatype `var = VAR of string => num`; 97 (* RW_TAC std_ss (type_rws "var") (* or list_ss or arith_ss *) *) 177 new_infix("is_variant", ==`:var->var->bool`==, 450); 470 ���SUC(CARD (s:var -> bool))���] LESS_CASES) 541 THEN ASSUME_TAC (INST_TYPE[==`:'a`== |-> ==`:var`==] FINITE_EMPTY) 584 THEN EXISTS_TAC ���s:var -> bool��� 687 THEN IMP_RES_THEN (ASSUME_TAC o SPEC ���x:var���) variant_THM 745 THEN EXISTS_TAC ���(y:var) INSERT s��� 849 THEN (MP_TAC o SPECL[���x:(var)lis [all...] |
/seL4-l4v-10.1.1/HOL4/src/simp/src/ |
H A D | congLib.sml | 62 val var = mk_var ("x", hol_type) value 64 val reflThm = refl {Rinst=preorderTerm,arg=var} 75 val var = mk_var ("x", hol_type) value 77 val reflThm = refl {Rinst=preorderTerm,arg=var}
|
/seL4-l4v-10.1.1/HOL4/examples/pgcl/src/ |
H A D | wpTools.sml | 103 val var = genvar (type_of wlp_post) value 104 val query = mk_leq (var, wlp_post) 105 val result = hd (snd (vc_solve (([var],[]),[query]))) 123 val _ = is_var la orelse raise ERR "dest_lam" "lhs rator not var"
|
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/ |
H A D | Thm.sig | 74 val freeIn : Term.var -> thm -> bool
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Thm.sig | 74 val freeIn : Term.var -> thm -> bool
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/x86/ |
H A D | prog_x86Lib.sml | 43 val var = mk_var(name_for_resource x name, type_of pattern) value 44 in mk_eq(subst [lhs |-> name] pattern,var) end 71 fun mk_pre_post_assertion (name,var) = let 77 else if type_of var = ``:word8`` then 79 else if type_of var = ``:word32`` then 81 in (subst [name_tm|->name,var_tm|->var] pattern, 82 subst [name_tm|->name,var_tm|->get_assigned_value name var] pattern) end
|
/seL4-l4v-10.1.1/HOL4/src/lite/ |
H A D | liteLib.sml | 417 fun MK_ABS_CONV var tm = 418 if (Term.is_comb tm andalso (Term.rand tm = var) 419 andalso not (Term.free_in var (Term.rator tm))) 422 let val rhs = Term.mk_abs(var,tm) 423 val newrhs = Term.mk_comb(rhs,var)
|
/seL4-l4v-10.1.1/HOL4/examples/acl2/ml/ |
H A D | testTypesScript.sml | 241 var = VAR of String; 248 val _ = AddType `:var`; 269 | VARatpat_e of var 281 | LAYEREDpat_e of var => pat_e; 291 | VARatexp_e of var long
|
/seL4-l4v-10.1.1/HOL4/src/temporal/src/ |
H A D | temporalLib.sml | 41 var of string | 102 in var(n) 178 | temporal2hol (var(x)) = mk_var{Name=x,Ty=(==`:num->bool`==)} 274 | var_names (var(x)) = [x] 328 | var(n) => var(n) 383 var(_) => ([],Phi) 421 val ell0 = var(ell0_name) 422 val ell1 = var(ell1_name) 432 val ell = var(ell_nam [all...] |
/seL4-l4v-10.1.1/HOL4/examples/temporal_deep/src/model_check/ |
H A D | modelCheckLib.sml | 255 if (((bdd.hash (bdd.high b) = 1) andalso (bdd.hash (bdd.low b) = 0))) then (num_to_var_string (bdd.var b)) else 256 if (((bdd.hash (bdd.high b) = 0) andalso (bdd.hash (bdd.low b) = 1))) then ("!"^(num_to_var_string (bdd.var b))) else 267 val var_s = num_to_var_string (bdd.var b); 270 ("("^(num_to_var_string (bdd.var b))^" | "^bdd_to_definition (low b)^")") else 272 ("(!"^(num_to_var_string (bdd.var b))^" | "^bdd_to_definition (high b)^")") else 274 ("(!"^(num_to_var_string (bdd.var b))^" & "^bdd_to_definition (low b)^")") else 276 ("("^(num_to_var_string (bdd.var b))^" & "^bdd_to_definition (high b)^")") else 484 fun varrenaming_foldr ((term, var), s) = 486 val x = "x"^(int_to_string var);
|
/seL4-l4v-10.1.1/HOL4/src/new-datatype/ |
H A D | NDatatype.sml | 337 val var = genvar ty value 338 in [(var, f var)] 342 val var = genvar a value 343 val inv = sumSyntax.mk_inl(var, b) 345 in (var, inv)::(div_sum_vars b f' (n-1))
|
/seL4-l4v-10.1.1/HOL4/src/portableML/poly/concurrent/ |
H A D | Task_Queue.sml | 62 status: exn option Synchronized.var} 67 fun new_group parent = make_group (parent, new_id (), Synchronized.var "group_status" NONE); 109 else SOME (Synchronized.var "timing" timing_start); 116 timing: timing Synchronized.var option} 140 val _ = (case timing of NONE => () | SOME var => Synchronized.change var (update t));
|
/seL4-l4v-10.1.1/HOL4/examples/lambda/basics/ |
H A D | generic_termsScript.sml | 21 pregterm = var string 'v 26 (fv (var s vv) = {s}) ��� 36 (���s vv. P (var s vv)) ��� 54 (raw_ptpm p (var s vv) = var (lswapstr p s) vv) ��� 116 (allatoms (var s vv) = {s}) ��� 171 (!s vv. aeq (var s vv) (var s vv)) /\ 185 ``~aeq (var s vv) (lam v bv ts us)``, 268 ``aeq (var v [all...] |
/seL4-l4v-10.1.1/HOL4/examples/CCS/ |
H A D | CCSScript.sml | 285 | var 'a 348 (CCS_Subst (var Y) E' X = if (Y = X) then E' else (var Y)) /\ 363 (* |- ���X E. CCS_Subst (var X) E X = E (2nd fixed point of CCS_Subst) *) 366 (REWRITE_CONV [CCS_Subst_def] ``CCS_Subst (var X) E X``)); 451 |- !X u E'. ~TRANS (var X) u E' 456 (Q.SPECL [`var X`, `u`, `E`] TRANS_cases))); 828 (FV (var X) = {X}) /\ 839 (BV (var X) = EMPTY) /\ 859 (CCS_Subst1 (var [all...] |
/seL4-l4v-10.1.1/HOL4/examples/HolBdd/ |
H A D | PrimitiveBddRules.sml | 256 (* replace b (makepairSet[(var b1, var b1'), ... , (var bi, var bi')]) *) 285 ((bdd.var b, bdd.var b')::replacel))) 331 (* (subst [v |-> tm1] tm2) |--> compose (var b, b1) b2 *) 344 bdd.compose (bdd.var b, b1) b2) 359 (* veccompose (composeSet (map (var ## I) [(b1,b1'), ... , (bi,bi')])) b *) 382 ((bdd.var [all...] |
/seL4-l4v-10.1.1/HOL4/src/HolQbf/ |
H A D | QbfCertificate.sml | 171 datatype vtype = Forall of term (* var *) 172 | Exists of (term * term) (* var, extvar *) 220 val (var,lits',deps) = value 231 in enum (insert(vars,vi,var)) t lits' deps (SOME vi) end 374 val var_dict = List.foldl (fn ((i, var, is_forall), var_dict) => 375 Redblackmap.insert (var_dict, var, (i, is_forall))) 377 fun index_fn var = 378 Redblackmap.find (var_dict, var)
|
/seL4-l4v-10.1.1/HOL4/src/HolSat/ |
H A D | minisatResolve.sml | 16 (*+1 because minisat var numbers start at 0,SatLib at 1*) 78 where v is the only var that occurs with opposite signs in c0 and c1 *)
|
/seL4-l4v-10.1.1/HOL4/src/real/ |
H A D | Diff.sml | 107 val var = variant (frees tm) lreal value 108 val tm2 = mk_comb(tm1,var)
|
/seL4-l4v-10.1.1/HOL4/examples/lambda/other-models/ |
H A D | swapScript.sml | 450 (!s p. rFV (var s p) SUBSET (s INSERT pFV p UNION X)) /\ 462 (rswap x y (var s p) = var (swapstr x y s) (pswap x y p))) /\ 476 (!s p. hom (VAR s) p = var s p) /\ 631 Q.INST [`var'` |-> `var`, `con'` |-> `con`, `app'` |-> `app`, 635 `var` |-> `\s p. var' s`,
|
/seL4-l4v-10.1.1/HOL4/src/compute/examples/ |
H A D | Arith.sml | 39 * strongly (arg of a free var), but we will have to reduce the
|
/seL4-l4v-10.1.1/HOL4/src/num/arith/src/ |
H A D | Sup_Inf.sml | 66 fun solve_ineqs ineqs var = 70 and (restl,restr) = solve_ineqs (tl ineqs) var 71 in (let val i = assoc var bind 74 (filter (fn (name,_) => not (name = var)) bind)
|
/seL4-l4v-10.1.1/HOL4/examples/muddy/ |
H A D | bvec.sml | 16 val var: precision -> varnum -> int -> bvec = app3 (symb "mlbvec_var") value
|