Searched refs:interpret (Results 1 - 18 of 18) sorted by last modified time

/seL4-l4v-master/HOL4/polyml/
H A Dconfigure5719 # Libtool will interpret -1 as no limit whatsoever
22056 polyarch=interpret
22063 polyarch=interpret
22069 polyarch=interpret
22075 polyarch=interpret
22081 polyarch=interpret
22087 polyarch=interpret
22093 polyarch=interpret
22099 polyarch=interpret
22105 polyarch=interpret
[all...]
/seL4-l4v-master/HOL4/polyml/libpolyml/
H A DMakefile.in154 x86assembly_gas64.S interpret.cpp x86assembly_gas32.S \
162 @ARCHI386_FALSE@@ARCHINTERPRET64_TRUE@@ARCHINTERPRET_FALSE@am__objects_1 = interpret.lo
163 @ARCHI386_FALSE@@ARCHINTERPRET_TRUE@am__objects_1 = interpret.lo
216 ./$(DEPDIR)/heapsizing.Plo ./$(DEPDIR)/interpret.Plo \
464 @ARCHI386_FALSE@@ARCHINTERPRET64_TRUE@@ARCHINTERPRET_FALSE@ARCHSOURCE = interpret.cpp
465 @ARCHI386_FALSE@@ARCHINTERPRET_TRUE@ARCHSOURCE = interpret.cpp
673 @AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/interpret.Plo@am__quote@ # am--include-marker
933 -rm -f ./$(DEPDIR)/interpret.Plo
1034 -rm -f ./$(DEPDIR)/interpret.Plo
/seL4-l4v-master/HOL4/src/postkernel/
H A DTheory.sml735 "Can't interpret pending loads"
/seL4-l4v-master/HOL4/examples/computability/recdegrees/
H A DrecdegreesScript.sml35 Definition interpret[simp]:
36 (interpret �� (BASE Ri n) <=>
38 (interpret �� (EXISTS v f) <=> ���n. interpret �����v���n��� f) ���
39 (interpret �� (ALL v f) <=> ���n. interpret �����v���n��� f)
45 ���x. x���A <=> interpret I���0���x��� (MKEA n Ri)
269 ���x. x ��� A ��� interpret I���0 ��� x��� (MKAE n Ri)
389 ���f. (interpret f (MKAE0 n k (lnot (lnot R))) = interpret
[all...]
/seL4-l4v-master/l4v/misc/vim/
H A Disabelle.vim73 syn keyword IsabelleCommand interpretation interpret
/seL4-l4v-master/graph-refine/
H A Drep_graph.py233 def interpret (self, rep): member in class:Hyp
649 # unreachable and we can't interpret all hyps
1066 return hyp.interpret (self)
/seL4-l4v-master/HOL4/tools/Holmake/poly/
H A DGraphExtra.sml29 | _ => die_with ("Can't interpret HOLHEAP spec. in " ^
H A DBuildCommand.sml436 (warn ("*** Couldn't interpret Moscow ML command: "^c);
/seL4-l4v-master/isabelle/src/Tools/jEdit/src/
H A Dscala_console.scala144 interp.interpret("import isabelle._; import isabelle.jedit._")
151 interp.interpret(command)
/seL4-l4v-master/l4v/isabelle/src/Tools/jEdit/src/
H A Dscala_console.scala144 interp.interpret("import isabelle._; import isabelle.jedit._")
151 interp.interpret(command)
/seL4-l4v-master/isabelle/src/Tools/Metis/src/
H A DModel.sml991 (* Taking apart terms to interpret them. *)
1029 fun interpret tm = function
1032 | Term.Fn (f,tms) => interpretFunction M (f, List.map interpret tms)
1034 interpret
1044 fun interpret V fm = function
1049 | Formula.Not p => not (interpret V p)
1050 | Formula.Or (p,q) => interpret V p orelse interpret V q
1051 | Formula.And (p,q) => interpret V p andalso interpret
[all...]
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/
H A DModel.sml991 (* Taking apart terms to interpret them. *)
1029 fun interpret tm = function
1032 | Term.Fn (f,tms) => interpretFunction M (f, List.map interpret tms)
1034 interpret
1044 fun interpret V fm = function
1049 | Formula.Not p => not (interpret V p)
1050 | Formula.Or (p,q) => interpret V p orelse interpret V q
1051 | Formula.And (p,q) => interpret V p andalso interpret
[all...]
/seL4-l4v-master/isabelle/src/Doc/Tutorial/document/
H A Dbasics.tex265 --- they were superfluous. If you are unsure how to interpret
/seL4-l4v-master/l4v/isabelle/src/Doc/Tutorial/document/
H A Dbasics.tex265 --- they were superfluous. If you are unsure how to interpret
/seL4-l4v-master/HOL4/src/quotient/Manual/
H A Dquotient.tex395 re-interpret this idea for type theory.
/seL4-l4v-master/HOL4/examples/
H A Dhol_dpllScript.sml357 (interpret f [] = T) /\
358 (interpret f (c::cs) = interpret_clause f c /\ interpret f cs)
364 ``!cs. MEM [] cs ==> ~interpret f cs``,
377 ``!cs v b. (f v = b) /\ interpret f cs ==>
378 interpret f (rewrite v b cs)``,
383 ``(find_uprop cs = SOME (q,r)) ==> ~interpret f (rewrite q (~r) cs)``,
396 ``!cs f. (dpll cs = NONE) ==> (interpret f cs = F)``,
409 `~interpret f (rewrite q (~r) cs)` by METIS_TAC [interpret_uprop] THEN
437 val th1 = SIMP_CONV (srw_ss()) [] ``interpret
[all...]
/seL4-l4v-master/HOL4/examples/formal-languages/regular/regular-play/src/
H A DregexMarkedScript.sml304 (* what is a state and what means a mark, what does this mean for final (how to interpret final) *)
/seL4-l4v-master/HOL4/Manual/Logic/
H A Dsemantics.tex512 is forced to interpret the new constants in the following way:
669 choice how to interpret the integers and their arithmetic in such a

Completed in 201 milliseconds