Searched refs:ac (Results 1 - 25 of 121) sorted by relevance

12345

/seL4-l4v-master/HOL4/src/simp/src/
H A DpureSimps.sml11 ac = [],
H A DcombinSimps.sml6 name = SOME "COMBIN", convs = [], congs = [], filter = NONE, ac = [],
H A DboolSimps.sml35 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 DsimpLib.sml92 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 Domega_automatonScript.sml174 `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 Dautomaton_formulaScript.sml1046 !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 Dmirror-website11 *.cl.cam.ac.uk)
/seL4-l4v-master/l4v/isabelle/Admin/Release/
H A Dmirror-website11 *.cl.cam.ac.uk)
/seL4-l4v-master/HOL4/examples/AKS/machine/
H A DcountMonadScript.sml54 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 Dprob_canonTools.sml13 ac = [],
/seL4-l4v-master/HOL4/examples/muddy/muddyC/buddy/src/
H A Dbddtest.cxx75 int main(int ac, char** av) argument
/seL4-l4v-master/HOL4/examples/unification/triangular/nominal/
H A DntermLib.sml6 val user_frag = ref (SSFRAG {dprocs = [], ac = [], rewrs = [],
15 fun congfrag ths = SSFRAG {dprocs = [], ac = [], rewrs = [],
/seL4-l4v-master/HOL4/src/coretypes/
H A DpairLib.sml119 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 Dsimplifier.sml30 rewrs = [], ac=[],filter=NONE,dprocs=[],congs=[]};
/seL4-l4v-master/HOL4/examples/muddy/muddyC/buddy/examples/queen/
H A Dqueen.cxx75 int main(int ac, char **av) argument
79 if (ac != 2)
/seL4-l4v-master/HOL4/src/pred_set/src/
H A Dpred_setSimps.sml12 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 Dextra_pred_setTools.sml40 {ac = [],
/seL4-l4v-master/HOL4/examples/ARM/v4/
H A DarmLib.sml25 rewrs = [], congs = [], filter = NONE, ac = [], dprocs = []};
62 filter = NONE, ac = [], dprocs = []};
/seL4-l4v-master/HOL4/examples/temporal_deep/src/model_check/
H A DibmScript.sml55 ``!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 Dverification.sml117 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 DbagSimps.sml12 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 Dselftest.sml66 ���[["acc"]; ["a"; "cc"]; ["ac"; "c"]; ["a"; "c"; "c"]]���;
70 ���[("","acc"); ("a","cc"); ("ac","c"); ("acc","")]���;
/seL4-l4v-master/HOL4/src/metis/
H A DnormalForms.sml219 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 DRandom.sml22 see http://random.mat.sbg.ac.at/~charly/server/server.html*)
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/
H A DRandom.sml22 see http://random.mat.sbg.ac.at/~charly/server/server.html*)

Completed in 594 milliseconds

12345