author | berghofe |
Tue, 13 Nov 2007 11:00:29 +0100 | |
changeset 25424 | 170f4cc34697 |
parent 25423 | 2c6167e2c587 |
child 25425 | 9191942c4ead |
--- a/src/HOL/Extraction.thy Tue Nov 13 10:59:26 2007 +0100 +++ b/src/HOL/Extraction.thy Tue Nov 13 11:00:29 2007 +0100 @@ -55,7 +55,7 @@ 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_rulify induct_rulify_fallback - True_implies_equals + True_implies_equals TrueE datatype sumbool = Left | Right