/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/ |
H A D | Rule.sig | 104 (* A rule takes one theorem and either deduces another or raises an Error *) 108 type rule = Thm.thm -> Thm.thm type 110 val allRule : rule 112 val noRule : rule 114 val thenRule : rule -> rule -> rule 116 val orelseRule : rule -> rule -> rule [all...] |
H A D | Rewrite.sig | 68 rewrite -> reductionOrder -> LiteralSet.set -> Rule.rule 70 val rewriteRule : rewrite -> reductionOrder -> Rule.rule 77 rewrite -> reductionOrder -> equationId -> LiteralSet.set -> Rule.rule 79 val rewriteIdRule : rewrite -> reductionOrder -> equationId -> Rule.rule 92 (* Rewriting as a derived rule. *)
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Rule.sig | 104 (* A rule takes one theorem and either deduces another or raises an Error *) 108 type rule = Thm.thm -> Thm.thm type 110 val allRule : rule 112 val noRule : rule 114 val thenRule : rule -> rule -> rule 116 val orelseRule : rule -> rule -> rule [all...] |
H A D | Rewrite.sig | 68 rewrite -> reductionOrder -> LiteralSet.set -> Rule.rule 70 val rewriteRule : rewrite -> reductionOrder -> Rule.rule 77 rewrite -> reductionOrder -> equationId -> LiteralSet.set -> Rule.rule 79 val rewriteIdRule : rewrite -> reductionOrder -> equationId -> Rule.rule 92 (* Rewriting as a derived rule. *)
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/hoare-triple/ |
H A D | helperLib.sig | 21 val RW : thm list -> rule 22 val RW1 : thm list -> rule 91 val BASIC_SEP_REWRITE_RULE : thm -> rule 92 val EXISTS_PRE : term frag list -> rule 93 val EXISTS_SEP_REWRITE_RULE : thm -> rule 94 val HIDE_POST_RULE : term -> rule 95 val HIDE_PRE_RULE : term -> rule 96 val HIDE_PRE_STATUS_RULE : thm -> rule 97 val HIDE_STATUS_RULE : bool -> thm -> rule 98 val INST_SPEC : thm -> rule [all...] |
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/m0/prog/ |
H A D | m0_progLib.sig | 7 val m0_introduction: Drule.rule 11 val memory_introduction: Drule.rule 13 val register_introduction: Drule.rule
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/common/ |
H A D | utilsLib.sig | 8 val ALL_HYP_CONV_RULE: conv -> rule 9 val ALL_HYP_RULE: rule -> rule 13 val ELIM_UNDISCH: rule 16 val HYP_CANON_RULE: rule 17 val HYP_CONV_RULE: conv -> term -> rule 18 val HYP_RULE: (thm -> thm) -> term -> rule 21 val INST_REWRITE_RULE: thm list -> rule 22 val LIST_DISCH: term list -> rule 23 val MATCH_HYP_CONV_RULE: conv -> term -> rule [all...] |
H A D | stateLib.sig | 6 val chunks_intro: bool -> thm -> rule 7 val chunks_intro_pre_process: thm -> rule 18 val introduce_triple_definition: bool * thm -> rule 19 val introduce_map_definition: thm * conv -> rule 28 val pick_endian_rule: (term -> bool) * rule * rule -> rule 38 val sep_array_intro: bool -> thm -> thm list -> rule 62 val MOVE_COND_RULE: term -> rule
|
H A D | spec_databaseLib.sig | 7 (''a -> ''a -> Drule.rule) -> (Thm.thm -> Term.term) ->
|
/seL4-l4v-10.1.1/HOL4/src/n-bit/ |
H A D | blastLib.sig | 6 val BBLAST_RULE : Conv.rule
|
/seL4-l4v-10.1.1/HOL4/tools/mlyacc/src/ |
H A D | core.sml | 29 { rule : rule, 34 val eqItem = fn (ITEM{rule=RULE{num=n,...},dot=d,...}, 35 ITEM{rule=RULE{num=m,...},dot=e,...}) => 38 val gtItem = fn (ITEM{rule=RULE{num=n,...},dot=d,...}, 39 ITEM{rule=RULE{num=m,...},dot=e,...}) => 68 in fn (ITEM {rule=RULE {lhs,rhs,rulenum,num,...}, 72 of nil => (print " (reduce by rule ";
|
H A D | lalr.sml | 114 (* look_pos: position in the rhs of a rule at which we should start placing 123 (* rule_pos: calculate place in the rhs of a rule at which we should start 133 rule has proven to be nullable so far. 155 val check_rule = fn (rule as RULE {num,...}) => 156 let val pos = rule_pos rule 158 prRule rule; 162 update(positions,num,rule_pos rule)) 171 fn (ITEM{rule,dot, rhsAfter=NONTERM _ :: _}) => 172 dot >= (look_pos rule) 189 map (fn rule [all...] |
/seL4-l4v-10.1.1/HOL4/examples/diningcryptos/ |
H A D | formalizeUseful.sig | 204 type rule = thm -> thm type 298 val THENR : rule * rule -> rule 299 val REPEATR : rule -> rule 300 val ORELSER : rule * rule -> rule 301 val TRYR : rule [all...] |
H A D | subtypeUseful.sig | 205 type rule = thm -> thm type 299 val THENR : rule * rule -> rule 300 val REPEATR : rule -> rule 301 val ORELSER : rule * rule -> rule 302 val TRYR : rule [all...] |
/seL4-l4v-10.1.1/HOL4/examples/miller/useful/ |
H A D | HurdUseful.sig | 201 type rule = thm -> thm type 294 val THENR : rule * rule -> rule 295 val REPEATR : rule -> rule 296 val ORELSER : rule * rule -> rule 297 val TRYR : rule [all...] |
/seL4-l4v-10.1.1/HOL4/src/floating-point/ |
H A D | lift_machine_ieeeScript.sml | 16 val rule = value 133 rule fp16_float_add_relative) 136 rule fp16_float_sub_relative) 139 rule fp16_float_mul_relative) 142 rule fp16_float_mul_add_relative) 145 rule fp16_float_mul_sub_relative) 148 rule fp16_float_div_relative) 151 rule fp16_float_sqrt_relative) 237 rule fp32_float_add_relative) 240 rule fp32_float_sub_relativ [all...] |
/seL4-l4v-10.1.1/HOL4/src/list/src/ |
H A D | numposrepLib.sml | 17 val rule = simpLib.SIMP_RULE numLib.std_ss [] value 19 fun l2n_pow2 i = rule (Thm.SPEC (f i) thm) 20 fun n2l_pow2 i = rule (Thm.SPEC (f i) n2l_pow2_compute)
|
/seL4-l4v-10.1.1/HOL4/src/res_quan/src/ |
H A D | res_quanLib.sig | 59 val RESQ_HALF_SPEC : term -> rule 60 val RESQ_HALF_SPECL : term list -> rule 61 val RESQ_SPEC : term -> rule 62 val RESQ_SPECL : term list -> rule 106 val Q_RESQ_HALF_SPEC : term quotation -> rule 107 val Q_RESQ_HALF_SPECL : term quotation list -> rule 108 val Q_RESQ_SPEC : term quotation -> rule 109 val Q_RESQ_SPECL : term quotation list -> rule 110 val Q_RESQ_HALF_ISPEC : term quotation -> rule 111 val Q_RESQ_HALF_ISPECL : term quotation list -> rule [all...] |
/seL4-l4v-10.1.1/HOL4/examples/dev/sw2/ |
H A D | patternMatch.sml | 44 | Leaf of rule_type list (* a single rule *) 67 fun relevant_indices(test_set, rule) = 72 (index = fst rule) andalso 73 not (match_constr (List.nth(snd rule, index), name))) test_list 95 (* Eliminate redundant rules in a rule list. *) 130 (* Modify the rule by instantializing it with constructor information. *) 133 fun inst_rule (rule : rule_type, index, subterm) = 134 (#1(rule), List.take(#2 rule, index) @ [subterm] @ List.drop(#2 rule, inde [all...] |
/seL4-l4v-10.1.1/HOL4/src/quotient/examples/ |
H A D | ind_rel.sig | 1 (* Subject: Mutually recursive rule induction *) 11 Term.term list (* each term corresponds to a quantified rule *)
|
/seL4-l4v-10.1.1/HOL4/examples/MLsyntax/ |
H A D | MLScript.sml | 39 * match ::= <rule> * 40 * | <rule> "|" <match> * 42 * rule ::= <pat> "=>" <exp> * 85 match = match rule 86 | matchl rule match ; 88 rule = rule pat exp ; 119 (ruleV (rule p e) = (patV p) UNION (expV e))
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/arm/prog/ |
H A D | arm_progLib.sig | 10 val change_config_rule: Drule.rule
|
/seL4-l4v-10.1.1/HOL4/examples/ARM/arm6-verification/ |
H A D | armLib.sig | 17 val UNABBREV_RULE : term frag list -> rule
|
/seL4-l4v-10.1.1/HOL4/examples/ARM/v4/ |
H A D | armLib.sig | 15 val UNABBREV_RULE : term frag list -> rule
|
/seL4-l4v-10.1.1/HOL4/src/datatype/mutrec/examples/ |
H A D | var_example.sml | 29 [{name = "match", arg_info = [being_defined "rule"]}, 30 {name = "match_list", arg_info = [being_defined "rule", 32 {type_name = "rule", 34 [{name = "rule", arg_info = [being_defined "pat", 90 (ruleV (rule p e) = (patV p) UNION (expV e))
|