| /seL4-l4v-10.1.1/HOL4/src/list/examples/ |
| H A D | test.sml | 126 val db = list_thm_database (); value
|
| /seL4-l4v-10.1.1/HOL4/src/Boolify/test/ |
| H A D | test.sml | 38 val db = TypeBase.theTypeBase() value
|
| /seL4-l4v-10.1.1/HOL4/help/src-sml/ |
| H A D | MyDatabase.sml | 46 val db = input_value is : database value
|
| H A D | Printbase.sml | 10 val db = readbase sigfile value
38 val db = readbase sigfile value
|
| H A D | HOLPage.sml | 49 = let val db = readbase dbfile value
|
| H A D | makebase.sml | 185 val db = mkbase res value
|
| H A D | Htmlsigs.sml | 334 val db = readbase helpfile value
351 val db = readbase sigfile value
[all...] |
| /seL4-l4v-10.1.1/HOL4/src/compute/src/ |
| H A D | clauses.sig | 33 and db = type
|
| H A D | equations.sml | 90 Cst (hc,r) => let val (db,b) = !r in CST{Head=hc, Args=[], Rws= db, Skip = b} end value
|
| H A D | clauses.sml | 119 and db = type
192 val (db, sk) = !rl value
199 val (db,_) = !rl value
308 fun db_of_entry (ss, r) = let val (db,opt) = !r in db end value
339 fun db_of_entry (ss, r) = let val (db,opt) = !r in (ss,db) end value
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/common/ |
| H A D | spec_databaseLib.sml | 61 val db = ref (LVTermNet.empty: (''opt entry) LVTermNet.lvtermnet) value
[all...] |
| /seL4-l4v-10.1.1/HOL4/src/boss/ml_evaluation/ |
| H A D | Lift.sml | 86 val db = TypeBase.theTypeBase() value
|
| /seL4-l4v-10.1.1/HOL4/src/postkernel/ |
| H A D | DB.sml | 191 | _ => let val db = CT() value
234 val db = CT() value
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/misc/ |
| H A D | wardScript.sml | 140 val db = let value
|
| /seL4-l4v-10.1.1/HOL4/polyml/libpolyml/ |
| H A D | reals.cpp | 152 union db { double dble; byte bytes[DBLE]; }; union
|
| H A D | realconv.cpp | 1480 U da, db; variable
1484 dval(&db) = b2d(b, &kb); variable
1498 word0(&db) += (k >> 2)*Exp_msk1; variable
1507 word0(&db) += k*Exp_msk1; variable
|
| /seL4-l4v-10.1.1/HOL4/src/Boolify/src/ |
| H A D | Encode.sml | 248 val db = TypeBase.theTypeBase () value
|
| /seL4-l4v-10.1.1/HOL4/src/datatype/ |
| H A D | Datatype.sml | 931 val (db, tyinfos) = f prevtypes db newastls value
994 val (db, new_tyinfos) = prim_define_type_from_astl prevtypes f db astl value
[all...] |