| /seL4-l4v-master/HOL4/src/bool/ |
| H A D | boolScript.sml | 419 val tb = Bv "t" value
[all...] |
| /seL4-l4v-master/HOL4/tools/Holmake/poly/ |
| H A D | MB_Monitor.sml | 220 val tb = tailbuffer.new { value
[all...] |
| /seL4-l4v-master/HOL4/examples/HolBdd/ |
| H A D | PrimitiveBddRules.sml | 308 val tb = tb1 and tbl = [(tbx,tbp),(tby,tbq)]; value
309 val tb = BddReplace tbl tb; value
311 val tb = tb1 and tbl = [(tbx,tby),(tby,tbz),(tbz,tbx)]; value
312 val tb = BddReplace tbl tb; value
314 val tb = tb1 and tbl = [(tbx,tby),(tby,tbz)]; value
315 val tb value
318 val tb = tb1 and tbl = [(tbx,tby),(tby,tbx)]; value
319 val tb = BddReplace tbl tb; value
321 val tb = tb1 and tbl = [(tbx,tbp),(tby,tbp)]; value
406 val tb = tb1 and tbl = [(tbx,tbp),(tby,tbq)]; value
407 val tb = BddListCompose tbl tb; value
409 val tb = tb1 and tbl = [(tbx,tby),(tby,tbz),(tbz,tbx)]; value
410 val tb = BddListCompose tbl tb; value
412 val tb = tb1 and tbl = [(tbx,tby),(tby,tbz)]; value
413 val tb = BddListCompose tbl tb; value
415 val tb = tb1 and tbl = [(tbx,tby),(tby,tbx)]; value
416 val tb = BddListCompose tbl tb; value
418 val tb = tb1 and tbl = [(tbx,tbp),(tby,tbp)]; value
[all...] |
| H A D | DerivedBddRules.sml | 718 let val tb = value
[all...] |
| /seL4-l4v-master/HOL4/examples/HolBdd/Examples/Solitaire/ |
| H A D | MiniTLHexSolitaireScript.sml | 243 val tb = GenTermToTermBdd (BddApRestrict ReachTb) hexsolitaire_varmap t2 value
334 val tb = GenTermToTermBdd (BddApRestrict ReachTb) hexsolitaire_varmap t2 value
|
| /seL4-l4v-master/isabelle/lib/browser/GraphBrowser/ |
| H A D | GraphBrowser.java | 24 TreeBrowser tb=null; field in class:GraphBrowser
|
| H A D | GraphView.java | 24 TreeBrowser tb; field in class:GraphView
|
| /seL4-l4v-master/l4v/isabelle/lib/browser/GraphBrowser/ |
| H A D | GraphBrowser.java | 24 TreeBrowser tb=null; field in class:GraphBrowser
|
| H A D | GraphView.java | 24 TreeBrowser tb; field in class:GraphView
|
| /seL4-l4v-master/HOL4/tools/Holmake/ |
| H A D | tailbuffer.sml | |
| /seL4-l4v-master/HOL4/src/opentheory/postbool/ |
| H A D | Logging.sml | 531 val tb = subst [tv|->vv] tb value
|
| /seL4-l4v-master/HOL4/src/finite_maps/ |
| H A D | enumTacs.sml | 781 val tb = rand (concl (DISPLAY_TO_ENUMERAL_CONV value
|
| /seL4-l4v-master/HOL4/examples/l3-machine-code/arm/model/ |
| H A D | arm.sml | 12161 val tb = BitsN.fromBitstring([tb'0],1) value
20623 val tb = BitsN.bits(1,1) typ value
|
| /seL4-l4v-master/HOL4/examples/HolCheck/ |
| H A D | muCheck.sml | 145 val tb = if (Option.isSome absf) then (* FIXME: can we remove the reference to absf? *) value
295 let val (tb,gth,sth,env,ix,rsc,ithm,abthm,ado_subthm,ado_eqthm) = !cch value
312 then let val tb = tb_func mf (Option.valOf sth) value
322 val tb = tb_func mf sth value
332 val tb = tb_func mf sth value
355 val tb = BddEqMp sithm (Option.valOf tb) value
364 val tb = tb_func mf sth value
372 val tb = tb_func mf sth value
396 val tb = cache_get cch ie (mk_ap_tb vm absf) (mk_gen_ap_thm ksname state msa) dp [] mf seth sel state value
401 val tb = cache_get cch ie (mk_rv_tb ee (!cch)) (mk_rv_spec_thm msr seth sel msreq ie ee state (!cch) dp) dp [] value
408 val tb = cache_get cch ie (BinExp (args,(seth,sel,state,ie)) bdd.And (snd(strip_comb(mf))) vm (f1,f2) dp abthm) value
416 val tb = cache_get cch ie (BinExp (args,(seth,sel,state,ie)) bdd.Or (snd(strip_comb(mf))) vm (f1,f2) dp abthm) value
424 val tb = cache_get cch ie (NotExp (args,(seth,sel,state,ie)) mf1 vm dp f1 abthm) value
434 val tb = cache_get cch ie (ModalExp (args,(seth,sel,state,ie)) act false (List.last(snd(strip_comb mf))) value
441 val tb = cache_get cch ie (ModalExp (args,(seth,sel,state,ie)) act true (List.last(snd(strip_comb mf))) value
449 val tb = cache_get cch ie (FixExp (args,(seth,sel,state,ie)) [rvnm,cabthmnm] (BddCon false vm) vm value
457 val tb = cache_get cch ie (FixExp (args,(seth,sel,state,ie)) [rvnm,cabthmnm] (BddCon true vm) vm value
465 val tb = BddNot (muCheck_aux (args,(seth,sel,state,ie)) mf1 vm dp f1) value
490 val tb =BddEqMp opthm bb value
959 val tb = muCheck_aux (init_stuff,(seth,sel,state,ie)) mf vm ((Array.length ee)-1) mfml value
[all...] |
| H A D | modelTools.sml | 155 then let val (tb,th,tr) = r value
|
| H A D | lazyTools.sml | 98 val tb = BddEqMp (MP (Drule.ISPECL [concl th,getTerm ltb] mp_thm) th) value
|
| H A D | ksTools.sml | 424 val tb = t2tb vm eq value
|
| H A D | ctlTools.sml | 50 val tb = BddForall st (BddExists st' Rtb) value
|
| H A D | ctlCheck.sml | 80 val ((tb,resthm,trace),(aic,cc)) = absCheck I1 [(".",#6(valOf(#ks(ic))))] state Ric vm ksname (#abs(ic),cc) (nf,mf) (apl,apsubs) value
|
| H A D | cearTools.sml | 708 val ((tb,tbt value
[all...] |