/seL4-l4v-10.1.1/HOL4/examples/hardware/hol88/mos-count/ |
H A D | gates.ml | 69 let Def = definition `dataabs` `Def`;; 79 Def (i t) ==> 80 Def (o t) /\ (BoolAbs (o t) = inv (BoolAbs (i t)))", 85 PURE_REWRITE_TAC [Def] THEN 95 Def (i1 t) /\ Def (i2 t) ==> 96 Def (o t) /\ 102 PURE_REWRITE_TAC [Def] THEN 112 Def (i [all...] |
H A D | dataabs.ml | 10 % logic to booleans. The predicates Def and Defn % 16 % The Def predicate is taken from Inder Dhingra's % 31 let Def = new_definition ( var 32 `Def`, 33 "Def (v:^val) = (v = Lo) \/ (v = Hi)");; 37 "(Defn 0 (v:^vec) = Def (v 0)) /\ 38 (Defn (SUC n) (v:^vec) = Def (v (SUC n)) /\ Defn n v)");; 80 GEN_ALL (fst (EQ_IMP_RULE Def)));;
|
H A D | halfaddn.ml | 56 Def (i t) /\ Def (cin t) ==> 57 Def (sum t) /\ Def (cout t) /\ 93 Defn n (i t) /\ Def (cin t) ==> 94 Defn n (sum t) /\ Def (cout t) /\
|
H A D | muxn.ml | 52 let Def = definition `dataabs` `Def`;; 81 Def (cntl t) /\ (cntlbar t = Not (cntl t)) 98 Def (cntl t) /\ (cntlbar t = Not (cntl t)) 115 ([],"!i o. INV_IMP (i,o) ==> !t. Def (i t) ==> (o t = Not (i t))"), 129 !t. Def (cntl t) ==> (o t = mux (BoolAbs (cntl t),i1 t,i2 t))",
|
H A D | incn.ml | 25 let Def = definition `dataabs` `Def`;; 34 ([],"!w. Vdd w ==> !t. Def (w t) /\ (BoolVal (BoolAbs (w t)) = 1)"), 37 ASM_REWRITE_TAC [Def;BoolVal;BoolAbs_THM]);;
|
H A D | count.ml | 63 Def ((reset when (isHi clk)) t) /\ 101 (!t. Def ((reset when (isHi clk)) t)) /\ 150 (!t. sysinit <= t ==> Def ((reset when (isHi clk)) t)) /\
|
H A D | toplevel.ml | 20 (!t. Def ((o when (isHi g)) t)) /\ 76 Def (w t) ==> (b t = BoolAbs (w t)) ==> (b t = T) ==> (w t = Hi)"),
|
/seL4-l4v-10.1.1/HOL4/src/postkernel/ |
H A D | DB_dtype.sml | 4 datatype class = Thm | Axm | Def
|
H A D | DB.sml | 27 | indef_class2string Def = "a definition" 136 (bind_with_classfn thyname Def (rev (Theory.current_definitions ())) o 256 val definitions = List.map thm_of o Lib.filter (is Def) o thy 270 if c = Def then thm
|
H A D | TheoryReader.sml | 208 | [s,"Def"] => 210 (name,Redblackmap.find (thmdict,name),DB.Def)
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/m0/model/ |
H A D | m0Script.sml | 136 val raise'exception_def = Def 146 val rec'PRIMASK_def = Def 151 val reg'PRIMASK_def = Def 157 val write'rec'PRIMASK_def = Def 161 val write'reg'PRIMASK_def = Def 165 val rec'PSR_def = Def 174 val reg'PSR_def = Def 186 val write'rec'PSR_def = Def 190 val write'reg'PSR_def = Def 194 val rec'CONTROL_def = Def [all...] |
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/x64/model/ |
H A D | x64Script.sml | 173 val raise'exception_def = Def 183 val DE_exception_def = Def 192 val UD_exception_def = Def 201 val GP_exception_def = Def 210 val XM_exception_def = Def 219 val rec'MXCSR_def = Def 232 val reg'MXCSR_def = Def 248 val write'rec'MXCSR_def = Def 252 val write'reg'MXCSR_def = Def 256 val mem8_def = Def [all...] |
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.1/ |
H A D | ILTheory.sml | 5208 [("MREG_TY_DEF",MREG_TY_DEF,DB.Def), ("MREG_BIJ",MREG_BIJ,DB.Def), 5209 ("R0",R0,DB.Def), ("R1",R1,DB.Def), ("R2",R2,DB.Def), ("R3",R3,DB.Def), 5210 ("R4",R4,DB.Def), ("R5",R5,DB.Def), ("R6",R6,DB.Def), ("R7",R7,DB.Def), [all...] |
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/mips/model/ |
H A D | mipsScript.sml | 306 val raise'exception_def = Def 316 val rec'Index_def = Def 322 val reg'Index_def = Def 328 val write'rec'Index_def = Def 332 val write'reg'Index_def = Def 336 val rec'Random_def = Def 341 val reg'Random_def = Def 347 val write'rec'Random_def = Def 351 val write'reg'Random_def = Def 355 val rec'Wired_def = Def [all...] |
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/cheri/ |
H A D | cheriScript.sml | 446 val raise'exception_def = Def 456 val rec'EntryLo_def = Def 464 val reg'EntryLo_def = Def 474 val write'rec'EntryLo_def = Def 478 val write'reg'EntryLo_def = Def 482 val rec'Index_def = Def 488 val reg'Index_def = Def 495 val write'rec'Index_def = Def 499 val write'reg'Index_def = Def 503 val rec'Random_def = Def [all...] |
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/riscv/model/ |
H A D | riscvScript.sml | 360 val raise'exception_def = Def 384 val archBase_def = Def 391 val architecture_def = Def 409 val archName_def = Def 416 val privLevel_def = Def 424 val privilege_def = Def 432 val privName_def = Def 440 val vmType_def = Def 463 val isValidVM_def = Def 469 val vmMode_def = Def [all...] |
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/arm/model/ |
H A D | armScript.sml | 347 val raise'exception_def = Def 357 val ArchVersion_def = Def 372 val HaveDSPSupport_def = Def 382 val HaveThumb2_def = Def 391 val HaveThumbEE_def = Def 404 val HaveMPExt_def = Def 414 val HaveSecurityExt_def = Def 425 val HaveVirtExt_def = Def 435 val rec'PSR_def = Def 448 val reg'PSR_def = Def [all...] |
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/arm8/model/ |
H A D | arm8Script.sml | 379 val raise'exception_def = Def 389 val rec'TCR_EL1_def = Def 396 val reg'TCR_EL1_def = Def 404 val write'rec'TCR_EL1_def = Def 408 val write'reg'TCR_EL1_def = Def 412 val rec'TCR_EL2_EL3_def = Def 419 val reg'TCR_EL2_EL3_def = Def 427 val write'rec'TCR_EL2_EL3_def = Def 431 val write'reg'TCR_EL2_EL3_def = Def 435 val rec'SCTLRType_def = Def [all...] |
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/monadic-arm/ |
H A D | armScript.sml | 318 val raise'exception_def = Def 335 val ArchVersion_def = Def 351 val HaveDSPSupport_def = Def 362 val HaveThumb2_def = Def 372 val HaveThumbEE_def = Def 407 val HaveMPExt_def = Def 428 val HaveSecurityExt_def = Def 450 val HaveVirtExt_def = Def 471 val rec'PSR_def = Def 484 val reg'PSR_def = Def [all...] |
/seL4-l4v-10.1.1/HOL4/examples/temporal_deep/src/model_check/ |
H A D | ibmScript.sml | 1450 GSYM_NO_TAC 7 (*Def sv*) THEN 1451 NTAC 2 (GSYM_NO_TAC 2) (*Def f, f'*) THEN 1562 NTAC 3 (GSYM_NO_TAC 2) (*Def f, f', sv*) THEN 1743 GSYM_NO_TAC 6 (*Def sv*) THEN 1744 GSYM_NO_TAC 1 (*Def f*) THEN 1779 GSYM_NO_TAC 1 (*Def f*) THEN 1823 GSYM_NO_TAC 2 (*Def f*) THEN 1860 NTAC 2 (GSYM_NO_TAC 1) (*Def f, sv*) THEN
|
/seL4-l4v-10.1.1/HOL4/examples/temporal_deep/src/translations/ |
H A D | omega_automaton_translationsScript.sml | 1214 GSYM_NO_TAC 3 (*Def R*) THEN 1233 GSYM_NO_TAC 0 (*Def R*) THEN 1248 GSYM_NO_TAC 0 (*Def P*) THEN 1259 GSYM_NO_TAC 2 (*Def R*) THEN 1290 GSYM_NO_TAC 4 (*Def R*) THEN 1306 GSYM_NO_TAC 0 (*Def r*) THEN 1307 GSYM_NO_TAC 4 (*Def R*) THEN 1310 GSYM_NO_TAC 2 (*Def v*) THEN 1354 WEAKEN_NO_TAC 1 (*Def R*) THEN 1477 GSYM_NO_TAC 7 (*Def [all...] |
/seL4-l4v-10.1.1/HOL4/src/TeX/ |
H A D | mungeTools.sml | 7 datatype opt = Turnstile | Case | TT | Def | SpacedDef | TypeOf | TermThm 48 | "def" => SOME Def 468 if OptSet.has Def opts orelse OptSet.has SpacedDef opts then let
|
/seL4-l4v-10.1.1/isabelle/src/Pure/PIDE/ |
H A D | rendering.scala | 404 case Markup.Entity.Def(i) if focus(i) => Some((Nil, Some(Rendering.Color.entity))) 463 case Markup.Entity.Def(i) if check(true, i) => Some(serials + i) 491 case Markup.Entity.Def(i) if focus(i) => Some(true)
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/PIDE/ |
H A D | rendering.scala | 404 case Markup.Entity.Def(i) if focus(i) => Some((Nil, Some(Rendering.Color.entity))) 463 case Markup.Entity.Def(i) if check(true, i) => Some(serials + i) 491 case Markup.Entity.Def(i) if focus(i) => Some(true)
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/common/ |
H A D | Import.sig | 141 val Def : string * Term.term * Term.term -> Theory.thm value
|