equal
deleted
inserted
replaced
474 ML_setup {* |
474 ML_setup {* |
475 change_simpset (fn ss => ss delloop "split_all_tac"); |
475 change_simpset (fn ss => ss delloop "split_all_tac"); |
476 change_claset (fn cs => cs delSWrapper "split_all_tac"); |
476 change_claset (fn cs => cs delSWrapper "split_all_tac"); |
477 *} |
477 *} |
478 |
478 |
479 inductive2 |
479 inductive |
480 ax_derivs :: "prog \<Rightarrow> 'a triples \<Rightarrow> 'a triples \<Rightarrow> bool" ("_,_|\<turnstile>_" [61,58,58] 57) |
480 ax_derivs :: "prog \<Rightarrow> 'a triples \<Rightarrow> 'a triples \<Rightarrow> bool" ("_,_|\<turnstile>_" [61,58,58] 57) |
481 and ax_deriv :: "prog \<Rightarrow> 'a triples \<Rightarrow> 'a triple \<Rightarrow> bool" ("_,_\<turnstile>_" [61,58,58] 57) |
481 and ax_deriv :: "prog \<Rightarrow> 'a triples \<Rightarrow> 'a triple \<Rightarrow> bool" ("_,_\<turnstile>_" [61,58,58] 57) |
482 for G :: prog |
482 for G :: prog |
483 where |
483 where |
484 |
484 |