/seL4-l4v-10.1.1/HOL4/src/num/arith/Manual/ |
H A D | Makefile | 2 # 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 D | description.tex | 1 \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 D | condition_guard.c | 54 int arith(int x, int y) { function
|
/seL4-l4v-10.1.1/HOL4/examples/hardware/hol88/tamarack2/ |
H A D | div.ml | 28 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 D | mod.ml | 32 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 D | arith.ml | 10 % FILE : arith.ml % 19 new_theory `arith`;;
|
H A D | proof1.ml | 46 let LESS_LESS_MONO = theorem `arith` `LESS_LESS_MONO`;;
|
/seL4-l4v-10.1.1/HOL4/examples/hardware/hol88/computer/ |
H A D | proof2.ml | 37 (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 D | proof1.ml | 15 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 D | arith.ml | 3 % 'arith.ml' % 13 new_theory `arith`;;
|
/seL4-l4v-10.1.1/HOL4/Manual/Reference/ |
H A D | Makefile | 77 /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 D | Arith.sml | 2 (* FILE : arith.sml *)
|
H A D | selftest.sml | 26 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 D | arm_parserLib.sig | 99 ; can use expr for int arith
|
H A D | arm_disassemblerLib.sml | 309 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 D | intSimps.sml | 97 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 D | advanced.tex | 653 \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 D | foundations.tex | 187 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 D | advanced.tex | 653 \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 D | foundations.tex | 187 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 D | Z3_ProofParser.sml | 108 ("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 D | numerics.tex | 28 \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 D | numerics.tex | 28 \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 D | realSimps.sml | 386 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 D | BaseCodeTree.sml | 294 | ArbArith arith => BuiltIns.arithRepr arith
|