/seL4-l4v-master/HOL4/src/simp/src/ |
H A D | pureSimps.sml | 11 ac = [],
|
H A D | combinSimps.sml | 6 name = SOME "COMBIN", convs = [], congs = [], filter = NONE, ac = [],
|
H A D | boolSimps.sml | 35 rewrs = [], congs = [], filter = NONE, ac = [], dprocs = []} 52 ac = [], congs = [literal_cong], convs = [], filter = NONE, 86 congs = [literal_cong], filter = NONE, ac = [], dprocs = []}; 100 convs = [], rewrs = [], filter=NONE, ac=[], dprocs=[]} 110 rewrs = [], filter= NONE, ac = [], dprocs=[] 150 rewrs=[],filter=NONE,ac=[],dprocs=[],congs=[]}; 167 ac = [], congs = [let_cong], convs = [], filter = NONE, 262 ac = [], congs = [], 280 ac = [], congs = [], 307 ac [all...] |
H A D | simpLib.sml | 92 ac : (thm * thm) list, 101 fun SSFRAG {name,convs,rewrs,ac,filter,dprocs,congs} = 102 SSFRAG_CON {name = name, rewrs = rewrs, ac = ac, 107 val empty_ssfrag = SSFRAG{name = NONE, rewrs = [], convs = [], ac = [], 111 val {name,rewrs,convs,ac,filter,dprocs,congs, relsimps} = s 113 SSFRAG_CON {name = name, rewrs = f rewrs, convs = convs, ac = ac, 121 fun name_ss s (SSFRAG_CON {convs,rewrs,filter,ac,dprocs,congs,relsimps,...}) = 123 ac [all...] |
/seL4-l4v-master/HOL4/examples/temporal_deep/src/deep_embeddings/ |
H A D | omega_automatonScript.sml | 174 `EXISTENTIAL_OMEGA_AUTOMATON_SEM (A, ac) i = 176 EXPLICIT_ACCEPT_COND_SEM i w ac)`; 180 `UNIVERSAL_OMEGA_AUTOMATON_SEM (A, ac) i = 182 (EXPLICIT_ACCEPT_COND_SEM i w ac))`; 189 ``!A ac i. 190 ((EXISTENTIAL_OMEGA_AUTOMATON_SEM (A, ac) i = 191 ~(UNIVERSAL_OMEGA_AUTOMATON_SEM (A, EXPLICIT_ACCEPT_NOT ac) i)) /\ 192 ((UNIVERSAL_OMEGA_AUTOMATON_SEM (A, ac) i) = 193 ~EXISTENTIAL_OMEGA_AUTOMATON_SEM (A, EXPLICIT_ACCEPT_NOT ac) i))``, 208 !ac [all...] |
H A D | automaton_formulaScript.sml | 1046 !ac t i f. 1047 ACCEPT_COND_SEM_TIME t i (ACCEPT_VAR_RENAMING f ac) = 1048 ACCEPT_COND_SEM_TIME t (\n x. f x IN i n) ac 1428 !A A' f ac. 1430 DISJOINT (IMAGE f (SEMI_AUTOMATON_USED_INPUT_VARS A)) (ACCEPT_COND_USED_VARS ac) ==> 1431 !i. A_SEM i (A_NDET (A, ACCEPT_COND ac)) = 1434 (\x. (if x IN SEMI_AUTOMATON_USED_INPUT_VARS A then f x else x)) ac))) 1500 !A A' f ac. 1502 DISJOINT (IMAGE f (SEMI_AUTOMATON_USED_INPUT_VARS A)) (ACCEPT_COND_USED_VARS ac) ==> 1503 !i. A_SEM i (A_UNIV (A, ACCEPT_COND ac)) [all...] |
/seL4-l4v-master/isabelle/Admin/Release/ |
H A D | mirror-website | 11 *.cl.cam.ac.uk)
|
/seL4-l4v-master/l4v/isabelle/Admin/Release/ |
H A D | mirror-website | 11 *.cl.cam.ac.uk)
|
/seL4-l4v-master/HOL4/examples/AKS/machine/ |
H A D | countMonadScript.sml | 54 valueOf_def |- !ac. valueOf ac = FST ac 55 stepsOf_def |- !ac. stepsOf ac = case ac of (a,Count n) => n 56 bind_def |- !ac f. bind ac f = 57 case ac of 116 valueOf (ac [all...] |
/seL4-l4v-master/HOL4/examples/miller/prob/ |
H A D | prob_canonTools.sml | 13 ac = [],
|
/seL4-l4v-master/HOL4/examples/muddy/muddyC/buddy/src/ |
H A D | bddtest.cxx | 75 int main(int ac, char** av) argument
|
/seL4-l4v-master/HOL4/examples/unification/triangular/nominal/ |
H A D | ntermLib.sml | 6 val user_frag = ref (SSFRAG {dprocs = [], ac = [], rewrs = [], 15 fun congfrag ths = SSFRAG {dprocs = [], ac = [], rewrs = [],
|
/seL4-l4v-master/HOL4/src/coretypes/ |
H A D | pairLib.sml | 119 fun f tm ac vs = 121 then (mk_eq(vs, tm))::ac 125 val ac = f (mk_fst tm) ac a value 126 val ac = f (mk_snd tm) ac d value 127 in ac end
|
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.2/ |
H A D | simplifier.sml | 30 rewrs = [], ac=[],filter=NONE,dprocs=[],congs=[]};
|
/seL4-l4v-master/HOL4/examples/muddy/muddyC/buddy/examples/queen/ |
H A D | queen.cxx | 75 int main(int ac, char **av) argument 79 if (ac != 2)
|
/seL4-l4v-master/HOL4/src/pred_set/src/ |
H A D | pred_setSimps.sml | 12 ac = [(UNION_ASSOC, UNION_COMM), (INTER_ASSOC, INTER_COMM)] 51 ac = [], name = SOME "GSPEC_SIMP", congs = [],
|
/seL4-l4v-master/HOL4/examples/miller/formalize/ |
H A D | extra_pred_setTools.sml | 40 {ac = [],
|
/seL4-l4v-master/HOL4/examples/ARM/v4/ |
H A D | armLib.sml | 25 rewrs = [], congs = [], filter = NONE, ac = [], dprocs = []}; 62 filter = NONE, ac = [], dprocs = []};
|
/seL4-l4v-master/HOL4/examples/temporal_deep/src/model_check/ |
H A D | ibmScript.sml | 55 ``!A ac l. (IS_TOTAL_DET_SYMBOLIC_SEMI_AUTOMATON A /\ DISJOINT A.S (LTL_USED_VARS l)) ==> 58 (((A_SEM i (A_UNIV (A, ACCEPT_COND ac)) = LTL_SEM i l) = 59 LTL_SEM (INPUT_RUN_PATH_UNION A i w) (LTL_EQUIV (ACCEPT_COND_TO_LTL ac, l)))))``, 70 ACCEPT_COND_SEM (INPUT_RUN_PATH_UNION A i w) ac) = 71 ACCEPT_COND_SEM (INPUT_RUN_PATH_UNION A i w) ac` by METIS_TAC[] THEN 95 ``!A ac (l:'a ltl). (IS_TOTAL_DET_SYMBOLIC_SEMI_AUTOMATON A /\ DISJOINT A.S (LTL_USED_VARS l) /\ FINITE A.S /\ INFINITE (UNIV:'a set)) ==> 99 (((A_SEM i (A_UNIV (A, ACCEPT_COND ac)) = LTL_SEM i l) = 107 Q_SPECL_NO_ASSUM 0 [`A`, `ac`, `l`] THEN 111 `?pf DS. (pf, DS) = LTL_TO_GEN_BUECHI (LTL_EQUIV (ACCEPT_COND_TO_LTL ac,l)) F T` by METIS_TAC[PAIR] THEN 114 (ACCEPT_COND_USED_VARS ac) UNIO [all...] |
/seL4-l4v-master/HOL4/examples/pgcl/examples/ |
H A D | verification.sml | 117 Guards [((\v. ~(v"pc" = 1) /\ ~(v"cc" = 1)), (Assign "ac" (\v. 1))); 118 ((\v. ~(v"pc" = 2) /\ ~(v"cc" = 2)), (Assign "ac" (\v. 2))); 119 ((\v. ~(v"pc" = 3) /\ ~(v"cc" = 3)), (Assign "ac" (\v. 3)))]`; 124 else Assign "cc" (\v. if ~(v"cc" = 1) /\ ~(v"ac" = 1) then 1 125 else if ~(v"cc" = 2) /\ ~(v"ac" = 2) then 2 else 3)`;
|
/seL4-l4v-master/HOL4/src/bag/ |
H A D | bagSimps.sml | 12 ac = [(SPEC_ALL ASSOC_BAG_UNION, SPEC_ALL COMM_BAG_UNION)], 80 ac = [], congs = [], 141 ac = [], convs = [], filter = NONE, rewrs = [],
|
/seL4-l4v-master/HOL4/examples/formal-languages/regular/regular-play/ |
H A D | selftest.sml | 66 ���[["acc"]; ["a"; "cc"]; ["ac"; "c"]; ["a"; "c"; "c"]]���; 70 ���[("","acc"); ("a","cc"); ("ac","c"); ("acc","")]���;
|
/seL4-l4v-master/HOL4/src/metis/ |
H A D | normalForms.sml | 219 convs = [], rewrs = [], congs = [], filter = NONE, ac = [], dprocs = []}; 257 filter = NONE, ac = [], dprocs = []}; 285 rewrs = [], congs = [], filter = NONE, ac = [], dprocs = []}; 1043 ac = [], 1106 ac = [], 1279 val af as Formula (ac,_,_,_) = count_cnf vs a 1282 Formula (conj_count ac bc, vs, tm, Conj (af,bf)) 1287 val af as Formula (ac,_,_,_) = count_cnf vs a 1290 Formula (disj_count ac bc, vs, tm, Disj (af,bf)) 1295 val af as Formula (ac, [all...] |
/seL4-l4v-master/isabelle/src/Tools/Metis/src/ |
H A D | Random.sml | 22 see http://random.mat.sbg.ac.at/~charly/server/server.html*)
|
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Random.sml | 22 see http://random.mat.sbg.ac.at/~charly/server/server.html*)
|