Lines Matching defs:g1
123 val g1 = sys avoid sgty_exists v tm1
124 in inst_guess g1 [tm1, tm2] SIMPLE_GUESS_EXISTS_AND_1 end
137 val g1 = sys avoid sgty_forall v tm1
138 in inst_guess g1 [tm1, tm2] SIMPLE_GUESS_FORALL_OR_1 end
151 val g1 = sys avoid sgty_exists v tm1
152 in inst_guess g1 [tm1, tm2] SIMPLE_GUESS_FORALL_IMP_1 end
165 val g1 = GEN v' g0
170 val thm' = HO_MATCH_MP thm0 g1
178 val g1 = GEN v' g0
183 val thm' = HO_MATCH_MP thm0 g1