changeset 18511 | beed2bc052a3 |
parent 18456 | 8cc35e95450a |
child 18708 | 4b3dadb4fe33 |
--- a/src/HOL/Extraction.thy Fri Dec 23 17:37:54 2005 +0100 +++ b/src/HOL/Extraction.thy Fri Dec 23 18:36:26 2005 +0100 @@ -54,7 +54,7 @@ notE' impE' impE iffE imp_cong simp_thms induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq induct_forall_def induct_implies_def induct_equal_def induct_conj_def - induct_atomize induct_atomize_old induct_rulify induct_rulify_fallback + induct_atomize induct_rulify induct_rulify_fallback datatype sumbool = Left | Right