Searched refs:Def (Results 1 - 25 of 38) sorted by relevance

12

/seL4-l4v-10.1.1/HOL4/examples/hardware/hol88/mos-count/
H A Dgates.ml69 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 Ddataabs.ml10 % 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 Dhalfaddn.ml56 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 Dmuxn.ml52 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 Dincn.ml25 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 Dcount.ml63 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 Dtoplevel.ml20 (!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 DDB_dtype.sml4 datatype class = Thm | Axm | Def
H A DDB.sml27 | 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 DTheoryReader.sml208 | [s,"Def"] =>
210 (name,Redblackmap.find (thmdict,name),DB.Def)
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/m0/model/
H A Dm0Script.sml136 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 Dx64Script.sml173 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 DILTheory.sml5208 [("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 DmipsScript.sml306 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 DcheriScript.sml446 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 DriscvScript.sml360 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 DarmScript.sml347 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 Darm8Script.sml379 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 DarmScript.sml318 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 DibmScript.sml1450 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 Domega_automaton_translationsScript.sml1214 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 DmungeTools.sml7 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 Drendering.scala404 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 Drendering.scala404 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 DImport.sig141 val Def : string * Term.term * Term.term -> Theory.thm value

Completed in 191 milliseconds

12