Searched refs:arith (Results 1 - 25 of 45) sorted by relevance

12

/seL4-l4v-10.1.1/HOL4/src/num/arith/Manual/
H A DMakefile2 # Makefile for the arith library documentation
6 # Pathname to the arith help files
32 @echo "\chapter{ML Functions in the arith Library}">entries.tex
37 ${MAKEINDEX} arith.idx
39 arith:
40 latex arith.tex
43 dvips arith.dvi -o
46 pdflatex arith.tex
49 make clean; make tex; make arith; make index; make arith p
[all...]
H A Ddescription.tex1 \chapter{The arith Library}
3 This document describes the facilities provided by the \ml{arith} library
77 The \ml{arith} library can be loaded into a user's \HOL\ session using the
84 library~\cite{reduce} is loaded. The \ml{arith} library makes use of some of
86 \ml{arith} library are loaded into \HOL.
88 The following session shows how the \ml{arith} library may be loaded using
93 #load_library `arith`;;
94 Loading library `arith` ...
108 Library `arith` loaded.
/seL4-l4v-10.1.1/l4v/tools/autocorres/tests/examples/
H A Dcondition_guard.c54 int arith(int x, int y) { function
/seL4-l4v-10.1.1/HOL4/examples/hardware/hol88/tamarack2/
H A Ddiv.ml28 new_parent `arith`;;
32 let LESS_LESS_0 = theorem `arith` `LESS_LESS_0`;;
33 let LESS_ADD_SUC = theorem `arith` `LESS_ADD_SUC`;;
34 let LESS_MONO_MULT_EQ = theorem `arith` `LESS_MONO_MULT_EQ`;;
35 let UNIQUE_QUOTIENT_THM = theorem `arith` `UNIQUE_QUOTIENT_THM`;;
H A Dmod.ml32 new_parent `arith`;;
42 let ADD_SUB = theorem `arith` `ADD_SUB`;;
43 let LESS_LESS_0 = theorem `arith` `LESS_LESS_0`;;
44 let ADD_SUB_ASSOC = theorem `arith` `ADD_SUB_ASSOC`;;
45 let ADD_LESS_OR_EQ = theorem `arith` `ADD_LESS_OR_EQ`;;
46 let UNIQUE_REMAINDER_THM = theorem `arith` `UNIQUE_REMAINDER_THM`;;
H A Darith.ml10 % FILE : arith.ml %
19 new_theory `arith`;;
H A Dproof1.ml46 let LESS_LESS_MONO = theorem `arith` `LESS_LESS_MONO`;;
/seL4-l4v-10.1.1/HOL4/examples/hardware/hol88/computer/
H A Dproof2.ml37 (theorem `arith` `plus_0_2`);
38 (theorem `arith` `plus_1_2`);
39 (theorem `arith` `plus_2_2`);
40 (theorem `arith` `plus_3_2`);
41 (theorem `arith` `plus_0_10`);
42 (theorem `arith` `plus_1_10`);
43 (theorem `arith` `plus_2_10`);
44 (theorem `arith` `plus_3_10`);
45 (theorem `arith` `plus_4_10`);
46 (theorem `arith` `plus_5_1
[all...]
H A Dproof1.ml15 new_parent `arith`;;
28 (theorem `arith` `plus_0_2`);
29 (theorem `arith` `plus_1_2`);
30 (theorem `arith` `plus_2_2`);
31 (theorem `arith` `plus_3_2`);
32 (theorem `arith` `plus_0_10`);
33 (theorem `arith` `plus_1_10`);
34 (theorem `arith` `plus_2_10`);
35 (theorem `arith` `plus_3_10`);
36 (theorem `arith` `plus_4_1
[all...]
H A Darith.ml3 % 'arith.ml' %
13 new_theory `arith`;;
/seL4-l4v-10.1.1/HOL4/Manual/Reference/
H A DMakefile77 /bin/sh bin/doc-to-tex ${D2TSED} ${Helpd}/THEOREMS/arith theorems.tex
91 (cd $(THMDIR)arith; $(MAKEDOC) num) ;
92 (cd $(THMDIR)arith; $(MAKEDOC) prim_rec) ;
93 (cd $(THMDIR)arith; $(MAKEDOC) arithmetic) ;
/seL4-l4v-10.1.1/HOL4/src/num/arith/src/
H A DArith.sml2 (* FILE : arith.sml *)
H A Dselftest.sml26 val _ = pr "Testing arith on ground ctxt"
80 "Testing arith on nested COND clause"
/seL4-l4v-10.1.1/HOL4/examples/ARM/v7/
H A Darm_parserLib.sig99 ; can use expr for int arith
H A Darm_disassemblerLib.sml309 fun arith x = f (sflag x) (commy [register d, register n, m1]) function
314 of 0 => arith "and"
315 | 1 => arith "eor"
316 | 2 => arith "sub"
317 | 3 => arith "rsb"
318 | 4 => arith "add"
319 | 5 => arith "adc"
320 | 6 => arith "sbc"
321 | 7 => arith "rsc"
326 | 12 => arith "or
[all...]
/seL4-l4v-10.1.1/HOL4/src/integer/
H A DintSimps.sml97 src/num/arith/src/numSimps.sml
99 src/num/arith/src/Gen_arith.sml
/seL4-l4v-10.1.1/isabelle/src/Doc/Intro/document/
H A Dadvanced.tex653 \S\ref{polymorphic}, let us define the class $arith$ of arithmetic
655 \alpha$, for $\alpha{::}arith$. We introduce $arith$ as a subclass of
660 classes arith < term
661 consts "0" :: 'a::arith ("0")
662 "1" :: 'a::arith ("1")
663 "+" :: ['a::arith,'a] => 'a (infixl 60)
671 We can now obtain distinct versions of the constants of $arith$ by
672 declaring certain types to be of class $arith$. For example, let us
678 arities bool, nat :: arith
[all...]
H A Dfoundations.tex187 overloading.\index{overloading|bold} We could declare $arith$ to be the
191 {+},{-},{\times},{/} & :: & [\alpha{::}arith,\alpha]\To \alpha
193 If we declare new types $real$ and $complex$ of class $arith$, then we
202 its arity as $(arith)arith$. Then we could declare the constant
215 $\alpha{::}\{arith,ord\}$, which means $\alpha$ belongs to both $arith$ and
216 $ord$. Semantically the set $\{arith,ord\}$ should be understood as the
217 intersection of the sets of types represented by $arith$ and $ord$. Such
256 \Sigma & :: & [nat,nat, nat\To \alpha{::}arith] \T
[all...]
/seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Intro/document/
H A Dadvanced.tex653 \S\ref{polymorphic}, let us define the class $arith$ of arithmetic
655 \alpha$, for $\alpha{::}arith$. We introduce $arith$ as a subclass of
660 classes arith < term
661 consts "0" :: 'a::arith ("0")
662 "1" :: 'a::arith ("1")
663 "+" :: ['a::arith,'a] => 'a (infixl 60)
671 We can now obtain distinct versions of the constants of $arith$ by
672 declaring certain types to be of class $arith$. For example, let us
678 arities bool, nat :: arith
[all...]
H A Dfoundations.tex187 overloading.\index{overloading|bold} We could declare $arith$ to be the
191 {+},{-},{\times},{/} & :: & [\alpha{::}arith,\alpha]\To \alpha
193 If we declare new types $real$ and $complex$ of class $arith$, then we
202 its arity as $(arith)arith$. Then we could declare the constant
215 $\alpha{::}\{arith,ord\}$, which means $\alpha$ belongs to both $arith$ and
216 $ord$. Semantically the set $\{arith,ord\}$ should be understood as the
217 intersection of the sets of types represented by $arith$ and $ord$. Such
256 \Sigma & :: & [nat,nat, nat\To \alpha{::}arith] \T
[all...]
/seL4-l4v-10.1.1/HOL4/src/HolSmt/
H A DZ3_ProofParser.sml108 ("th-lemma-arith", list_prems "th-lemma-arith"),
292 ("th-lemma-arith", list_prems_pt TH_LEMMA_ARITH),
/seL4-l4v-10.1.1/isabelle/src/Doc/Tutorial/document/
H A Dnumerics.tex28 \methdx{arith}. Linear arithmetic comprises addition, subtraction
32 causes case splits. On types \isa{nat} and \isa{int}, \methdx{arith}
228 \isacommand{apply}\ (subgoal_tac\ "n=0\ |\ n=1",\ force,\ arith)\isanewline
247 The \isa{arith} method can prove facts about \isa{abs} automatically,
251 \isacommand{by}\ arith
/seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Tutorial/document/
H A Dnumerics.tex28 \methdx{arith}. Linear arithmetic comprises addition, subtraction
32 causes case splits. On types \isa{nat} and \isa{int}, \methdx{arith}
228 \isacommand{apply}\ (subgoal_tac\ "n=0\ |\ n=1",\ force,\ arith)\isanewline
247 The \isa{arith} method can prove facts about \isa{abs} automatically,
251 \isacommand{by}\ arith
/seL4-l4v-10.1.1/HOL4/src/real/
H A DrealSimps.sml386 src/num/arith/src/numSimps.sml
388 src/num/arith/src/Gen_arith.sml
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/CodeTree/
H A DBaseCodeTree.sml294 | ArbArith arith => BuiltIns.arithRepr arith

Completed in 108 milliseconds

12