| /seL4-l4v-10.1.1/HOL4/src/HolSmt/ |
| H A D | Z3_ProofReplay.sml | 539 val (lhs, rhs) = boolSyntax.dest_disj t value
571 val (lhs, rhs) = boolSyntax.dest_eq t value
720 val (lhs, rhs) = boolSyntax.dest_eq t value
|
| /seL4-l4v-10.1.1/HOL4/src/IndDef/ |
| H A D | IndDefRules.sml | 495 else let val (lhs,rhs) = dest_eq(concl(hd ths)) value
|
| /seL4-l4v-10.1.1/HOL4/src/datatype/mutrec/ |
| H A D | ConsThms.sml | 451 let val {lhs = x1, rhs = x2} = dest_eq (concl eq1) value
452 val {lhs = y1, rhs = y2} = dest_eq (concl eq2) value
460 let val {lhs = appl_cons_eq, rhs = args_eq} = dest_eq gl value
619 val {lhs = left, rhs = right} = dest_eq eq_term value
[all...] |
| /seL4-l4v-10.1.1/HOL4/src/datatype/record/ |
| H A D | RecordType.sml | 427 val lhs = mk_eq(var1, var2) value
|
| /seL4-l4v-10.1.1/HOL4/src/metis/ |
| H A D | mlibTerm.sml | 576 val lhs = fst o dest_eq; value
|
| /seL4-l4v-10.1.1/HOL4/src/parse/ |
| H A D | Preterm.sml | 44 val lhs = #1 o pdest_eq value
|
| H A D | Parse.sml | 38 fun lhs tm = #2(sdest_binop("=","min") (ERROR"lhs" "") tm); function
|
| /seL4-l4v-10.1.1/HOL4/src/q/ |
| H A D | Q.sml | 262 val (lhs,rhs) = dest_eq(concl th) value
269 let val (lhs,rhs) = dest_eq(concl th) value
|
| /seL4-l4v-10.1.1/HOL4/src/quotient/examples/ |
| H A D | tactics.sml | 258 let val (lhs,rhs) = dest_eq cnj value
|
| H A D | ind_rel.sml | 1167 else let val (lhs,rhs) = dest_eq(concl(hd ths)) value
|
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/compiler/ |
| H A D | reg_allocLib.sml | 213 val (lhs,rhs) = dest_eq x value
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/temporal_deep/src/translations/ |
| H A D | translationsLib.sml | 930 val lhs = rand (rator (concl imp_thm)) value
|
| /seL4-l4v-10.1.1/HOL4/examples/elliptic/c_output/ |
| H A D | c_outputLib.sml | 348 val (lhs, body) = pairLib.dest_pabs body; value
|
| /seL4-l4v-10.1.1/HOL4/src/1/ |
| H A D | Tactic.sml | 212 val (lhs, rhs) = dest_eq t value
346 val (lhs, rhs) = dest_eq (concl th) value
571 val (lhs, rhs) = with_exn dest_eq g (ERR "REFL_TAC" "not an equation") value
617 val (lhs, rhs) = with_exn dest_eq gl (ER "not an equation") value
642 val (lhs, rhs) = with_exn dest_eq gl (ER "not an equation") value
661 val (lhs, rhs) = with_exn dest_eq w (ER "not an equation") value
691 val (lhs, rhs) = with_exn dest_eq gl (ER "not an equation") value
[all...] |
| H A D | Conv.sml | 259 val {lhs, rhs} = dest_eq (concl th) value
1542 val {lhs, rhs} = dest_eq tm value
2208 val {lhs, rhs} = dest_eq tm value
[all...] |
| /seL4-l4v-10.1.1/HOL4/src/basicProof/ |
| H A D | BasicProvers.sml | 569 else let val (lhs,rhs) = dest_eq c value
583 let val (lhs,rhs) = dest_eq tm value
763 let val (lhs,rhs) = dest_eq tm value
[all...] |
| /seL4-l4v-10.1.1/HOL4/tools/Holmake/ |
| H A D | Holmake_tools.sml | 676 val lhs = Substring.string lhs0 value
|
| /seL4-l4v-10.1.1/HOL4/examples/theorem-prover/lisp-runtime/extract/ |
| H A D | lisp_extractLib.sml | 404 val lhs = foldl (fn (x,y) => mk_comb(y,x)) new_fun params value
492 val lhs = map (fn x => mk_comb(new_fun,x)) ps value
746 val lhs = foldl (fn (x,y) => mk_comb(y,x)) new_fun params value
774 val lhs value
914 val lhs = foldl (fn (x,y) => mk_comb(y,x)) new_fun params value
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/theorem-prover/lisp-runtime/implementation/ |
| H A D | lisp_compiler_opScript.sml | 2063 val (lhs,rhs) = hd xs value
2082 val (lhs,rh value
[all...] |
| /seL4-l4v-10.1.1/HOL4/src/boss/ |
| H A D | prove_base_assumsScript.sml | 531 val (lhs, rhs) = dest_eq (concl th) value
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/hoare-triple/ |
| H A D | helperLib.sml | 634 val lhs = fst (dest_eq (concl imp)) value
650 val lhs = mk_star(last vs,frame) value
1131 val lhs value
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/HolCheck/ |
| H A D | lzConv.sml | 259 val {lhs,rhs} = dest_eq (concl th) value
1353 let val {lhs,rhs} = dest_eq tm value
1566 let val {lhs,rhs} = dest_eq tm value
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/acl2/examples/M1/ |
| H A D | sexp.sml | 236 val (lhs,rhs) = dest_eq (spec_all hd_eqn) value
|
| /seL4-l4v-10.1.1/HOL4/examples/acl2/examples/acl2-hol-ltl-paper-example/ |
| H A D | sexp.sml | 236 val (lhs,rhs) = dest_eq (spec_all hd_eqn) value
|
| /seL4-l4v-10.1.1/HOL4/examples/acl2/ml/ |
| H A D | sexp.sml | 236 val (lhs,rhs) = dest_eq (spec_all hd_eqn) value
|