equal
deleted
inserted
replaced
112 val major::prems = goal Trancl.thy |
112 val major::prems = goal Trancl.thy |
113 "[| <a,b> : r^*; \ |
113 "[| <a,b> : r^*; \ |
114 \ !!x. P(<x,x>); \ |
114 \ !!x. P(<x,x>); \ |
115 \ !!x y z.[| P(<x,y>); <x,y>: r^*; <y,z>: r |] ==> P(<x,z>) |] \ |
115 \ !!x y z.[| P(<x,y>); <x,y>: r^*; <y,z>: r |] ==> P(<x,z>) |] \ |
116 \ ==> P(<a,b>)"; |
116 \ ==> P(<a,b>)"; |
117 by (rtac (major RS (rtrancl_def RS def_induct)) 1); |
117 by (rtac ([rtrancl_def, rtrancl_fun_mono, major] MRS def_induct) 1); |
118 by (rtac rtrancl_fun_mono 1); |
|
119 by (fast_tac (comp_cs addIs prems) 1); |
118 by (fast_tac (comp_cs addIs prems) 1); |
120 val rtrancl_full_induct = result(); |
119 val rtrancl_full_induct = result(); |
121 |
120 |
122 (*nice induction rule*) |
121 (*nice induction rule*) |
123 val major::prems = goal Trancl.thy |
122 val major::prems = goal Trancl.thy |