/seL4-l4v-10.1.1/HOL4/src/tfl/src/ |
H A D | Induction.sml | 460 (* ?vlist. (var = tm) *) 461 (* ?vlist. (var = tm) /\ constraints (* literal pattern *) *)
|
/seL4-l4v-10.1.1/HOL4/examples/lambda/barendregt/ |
H A D | finite_developmentsScript.sml | 823 `?var b. M = LAM var b` by PROVE_TAC [term_CASES, is_abs_thm] THEN 844 `?var b. M = LAM var b` by PROVE_TAC [term_CASES, is_abs_thm] THEN 965 `?var b. M = LAM var b` by PROVE_TAC [term_CASES, is_abs_thm] THEN 1083 `?var b. t = LAM var b` by PROVE_TAC [term_CASES, is_abs_thm] THEN
|
H A D | normal_orderScript.sml | 970 `���var args. LAM v N0 = VAR var ���� args`
|
/seL4-l4v-10.1.1/HOL4/examples/HolCheck/ |
H A D | ksTools.sml | 111 andalso List.null (List.filter has_primed_vars args) (* neither lhs nor rhs contain a primed var *) 282 (* construct state var tuple from I and T*)
|
H A D | muCheck.sml | 198 andalso (Vector.sub(rsc,ix)>0)) (*i.e.current bnd var top level fv filt by >0 test*) 201 else (* otherwise not innermost bound var so must account for change in environment *) 566 (* create a new RV theorem for this bound var and add it to the spec thms, and add the bv's initbdd to the env *) 752 val mf = inst [alpha |-> prop_ty] mf (* it is possible that mf 's type var has not been instantiated *)
|
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/ |
H A D | texinfo.tex | 1400 % special-casing \var here? 1401 \def\var##1{##1}% 2385 % Unconditional use \ttsl, and no ic. @var is set to this for defuns. 2393 \def\var#1{% 2802 % an actual _ character, as in @math{@var{some_variable} + 1}. So make 2804 % which is what @var uses. 4598 \definedummyword\var 6946 % @deftypevr category type var args 6949 % @deftypecv category class type var args 6952 % \deftypecvof {category of}class type var arg [all...] |
H A D | configure | 939 localstatedir='${prefix}/var' 1491 --localstatedir=DIR modifiable single-machine data [PREFIX/var] 2756 ac_config_guess="$SHELL $ac_aux_dir/config.guess" # Please don't use this var. 2757 ac_config_sub="$SHELL $ac_aux_dir/config.sub" # Please don't use this var. 2758 ac_configure="$SHELL $ac_aux_dir/configure" # Please don't use this var. 3072 # Use test -z because SunOS4 sh mishandles braces in ${var-val}. 12243 sys_lib_search_path_spec="/usr/shlib /usr/ccs/lib /usr/lib/cmplrs/cc /usr/lib /usr/local/lib /var/shlib" 16220 sys_lib_search_path_spec="/usr/shlib /usr/ccs/lib /usr/lib/cmplrs/cc /usr/lib /usr/local/lib /var/shlib" 16652 echo "* CPU you have. (Set the CFLAGS environment var. *" 17218 cputype=`(((grep cpu /proc/cpuinfo | cut -d: -f2) ; ($PRTDIAG -v |grep -i sparc) ; grep -i cpu /var/ru [all...] |
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/ |
H A D | funCall.sml | 155 SUB sp, sp, #var (* skip local variables *)
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.1/ |
H A D | funCall.sml | 143 SUB sp, sp, #var (* skip local variables *)
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.2/ |
H A D | funCall.sml | 140 SUB sp, sp, #var (* skip local variables *)
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw2/ |
H A D | regAlloc.sml | 112 val live = (* set of registers already assigned to live var in cont *)
|
/seL4-l4v-10.1.1/HOL4/src/IndDef/ |
H A D | IndDefRules.sml | 74 (\arg1 .. argn. const arg1 .. argn /\ var arg1 .. argn) term1 .. termn
|
/seL4-l4v-10.1.1/HOL4/src/metis/ |
H A D | mlibClauseset.sml | 248 | Fn _ => raise Bug "new_pred: new_var didn't return a var";
|
/seL4-l4v-10.1.1/HOL4/src/pfl/ |
H A D | index.sml | 127 (* form (term,var), d is a list of terms, and vs is a list of used variables *)
|
/seL4-l4v-10.1.1/HOL4/src/postkernel/ |
H A D | HolKernel.sml | 669 else (* vtm not a var *) let
|
/seL4-l4v-10.1.1/HOL4/src/refute/ |
H A D | Canon.sml | 495 let val ((skol,v,var),rest) = Lib.pluck
|
/seL4-l4v-10.1.1/HOL4/src/experimental-kernel/ |
H A D | Term.sml | 920 NONE => (* var on left not bound *) let 936 else MERR "Bound var doesn't match"
|
/seL4-l4v-10.1.1/HOL4/examples/miller/ho_prover/ |
H A D | ho_proverTools.sml | 767 else raise ERR "equal_rule" "non-var = non-var"
|
/seL4-l4v-10.1.1/HOL4/examples/acl2/examples/M1/ |
H A D | hol_defaxiomsScript.sml | 2541 |- global_val var wrld = 2542 fgetprop var (asym "GLOBAL-VALUE") 3633 (let var = print_base in 3634 ite (integerp var) var 3635 (the_error (csym "INTEGER") var))) digits
|
/seL4-l4v-10.1.1/HOL4/examples/acl2/examples/acl2-hol-ltl-paper-example/ |
H A D | hol_defaxiomsScript.sml | 2503 |- global_val var wrld = 2504 fgetprop var (asym "GLOBAL-VALUE") 3595 (let var = print_base in 3596 ite (integerp var) var 3597 (the_error (csym "INTEGER") var))) digits
|
/seL4-l4v-10.1.1/HOL4/examples/acl2/ml/ |
H A D | hol_defaxiomsScript.sml | 2499 |- global_val var wrld = 2500 fgetprop var (asym "GLOBAL-VALUE") 3591 (let var = print_base in 3592 ite (integerp var) var 3593 (the_error (csym "INTEGER") var))) digits
|
/seL4-l4v-10.1.1/HOL4/polyml/ |
H A D | configure | 899 localstatedir='${prefix}/var' 1451 --localstatedir=DIR modifiable single-machine data [PREFIX/var] 2964 ac_config_guess="$SHELL $ac_aux_dir/config.guess" # Please don't use this var. 2965 ac_config_sub="$SHELL $ac_aux_dir/config.sub" # Please don't use this var. 2966 ac_configure="$SHELL $ac_aux_dir/configure" # Please don't use this var. 3054 # Use test -z because SunOS4 sh mishandles braces in ${var-val}. 12230 sys_lib_search_path_spec="/usr/shlib /usr/ccs/lib /usr/lib/cmplrs/cc /usr/lib /usr/local/lib /var/shlib" 16656 sys_lib_search_path_spec="/usr/shlib /usr/ccs/lib /usr/lib/cmplrs/cc /usr/lib /usr/local/lib /var/shlib" 23507 for var in AS \ 23607 case \`eval \\\\\$ECHO \\\\""\\\\\$\$var"\\\\"\` i [all...] |
/seL4-l4v-10.1.1/HOL4/examples/machine-code/hoare-triple/ |
H A D | helperLib.sml | 498 fun EXISTS_PRE var th = 500 val v = parse_in_thm var th
|
/seL4-l4v-10.1.1/HOL4/examples/diningcryptos/ |
H A D | formalizeUseful.sml | 657 val _ = assert (is_var tm) (ERR "dest_bv" "not a var")
|
H A D | subtypeUseful.sml | 655 val _ = assert (is_var tm) (ERR "dest_bv" "not a var")
|