Lines Matching defs:matcher
12 type matcher = name * pattern * bool (* whole term? *)
45 semantics of matcher list with a tactic (match_case):
49 - if failed, backtrack within current matcher;
50 - if no assumptions match, backtrack to previous matcher
51 3. Go to the next matcher
58 semantics of (matcher list * thms_tactic) list:
64 val match1_tac : matcher * mg_tactic -> tactic
66 val match_tac : matcher list * mg_tactic -> tactic
68 val first_match_tac : (matcher list * mg_tactic) list -> tactic
77 val a : string -> pattern -> matcher
80 val ua : pattern -> matcher
81 val au : pattern -> matcher
84 val ab : string -> pattern -> matcher
85 val ba : string -> pattern -> matcher
88 val uab : pattern -> matcher
89 val uba : pattern -> matcher
90 val aub : pattern -> matcher
91 val abu : pattern -> matcher
92 val bau : pattern -> matcher
93 val bua : pattern -> matcher
96 val c : pattern -> matcher
99 val cb : pattern -> matcher
100 val bc : pattern -> matcher
103 val ac : pattern -> matcher
104 val ca : pattern -> matcher
107 val acb : pattern -> matcher
108 val abc : pattern -> matcher
109 val bca : pattern -> matcher
110 val cba : pattern -> matcher
111 val cab : pattern -> matcher
112 val bac : pattern -> matcher