Lines Matching refs:priority
200 fun add_conditional_rewrite priority name thm =
217 a <= priority handle e => wrapException "add_conditional_rewrite" e
224 fun p (a,b,c) = "Rewrite: " ^ b ^ " with priority: " ^ int_to_string a ^ ":\n" ^ thm_to_string c ^ "\n"
250 (map (fn thm' => rewrites := Net.insert (lhs final,(priority:int,name:string,thm')) (!rewrites)) all_thms ; ())
289 fun add_standard_rewrite priority name thm =
293 add_conditional_rewrite priority name toadd
310 Net.filter (fn (priority,name,thm) => Theory.uptodate_thm thm)
846 fun instantiate_encoders (priority,name,thm) =
857 (priority,name,
1408 fun exists_polytypic_theorem previous (priority,name,theorem) =
1411 exists (fn (p,n,t) => (p = priority) andalso
1424 | ((priority,name,thm)::_) =>
1427 (add_conditional_rewrite priority name thm
1495 fun add_polytypic_rewrite priority name func =
1499 else polytypic_rewrites := (priority,name,func) :: (!polytypic_rewrites)
1505 fun add_standard_conversion priority name func =
1509 else conversions := (priority,name,conditionize_rewrite o func) ::
1512 fun add_conditional_conversion priority name func =
1516 else conversions := (priority,name,func) ::
2532 fun add_ifnew_standard_rewrite priority name thm =
2535 else add_standard_rewrite priority name thm
2536 fun add_ifnew_conditional_rewrite priority name thm =
2539 else add_conditional_rewrite priority name thm