Lines Matching defs:trans
41 val trans = (REWRITE_RULE [GSYM Reach_def]) o BETA_RULE o (ISPEC Reach_defn);
44 "Reach_trans", trans (REWRITE_RULE [transitive_def] RTC_TRANSITIVE));
47 "Reach_ind", trans RTC_INDUCT);
50 "Reach_strongind", trans RTC_STRONG_INDUCT);
53 "Reach_ind_right", trans RTC_INDUCT_RIGHT1);
56 "Reach_strongind_right", trans RTC_STRONG_INDUCT_RIGHT1);
59 "Reach_cases1", trans RTC_CASES1);
62 "Reach_cases2", trans RTC_CASES2);
136 val trans = (REWRITE_RULE [GSYM STEP_def]) o BETA_RULE o (ISPEC STEP_defn);
139 val STEP0 = save_thm ("STEP0", trans NRC_0);
142 val STEP1 = save_thm ("STEP1", trans (Q.GEN `R` NRC_1));
146 "STEP_SUC", trans (CONJUNCT2 NRC));
150 "STEP_SUC_LEFT", trans (Q_GENL [`R`, `n`, `x`, `y`] NRC_SUC_RECURSE_LEFT));
154 "STEP_ADD_E", trans (Q.GEN `R` NRC_ADD_E));
158 "STEP_ADD_EQN", trans (Q_GENL [`R`, `m`, `n`, `x`, `z`] NRC_ADD_EQN));
162 "STEP_ADD_I", trans (Q.GEN `R` NRC_ADD_I));
401 val trans = (REWRITE_RULE [SYM TRACE_def]) o (ISPEC ``TRANS``);
407 "TRACE_rules", trans LRTC_RULES);
411 "TRACE_trans", trans LRTC_LRTC);
417 "TRACE_ind", trans LRTC_INDUCT);
424 "TRACE_strongind", trans LRTC_STRONG_INDUCT);
430 "TRACE_cases1", trans LRTC_CASES1);
436 "TRACE_cases2", trans LRTC_CASES2);
441 "TRACE_cases_twice", trans LRTC_CASES_LRTC_TWICE);
445 "TRACE_APPEND_cases", trans LRTC_APPEND_CASES);
449 "TRACE_NIL", trans LRTC_NIL);
453 "TRACE1", trans LRTC_SINGLE);
457 "TRACE_ONE", trans LRTC_ONE);