equal
deleted
inserted
replaced
35 |
35 |
36 lemmas [extraction_expand_def] = |
36 lemmas [extraction_expand_def] = |
37 induct_forall_def induct_implies_def induct_equal_def induct_conj_def |
37 induct_forall_def induct_implies_def induct_equal_def induct_conj_def |
38 induct_true_def induct_false_def |
38 induct_true_def induct_false_def |
39 |
39 |
40 datatype (plugins only:) sumbool = Left | Right |
40 datatype (plugins only: code) sumbool = Left | Right |
41 |
41 |
42 subsection {* Type of extracted program *} |
42 subsection {* Type of extracted program *} |
43 |
43 |
44 extract_type |
44 extract_type |
45 "typeof (Trueprop P) \<equiv> typeof P" |
45 "typeof (Trueprop P) \<equiv> typeof P" |