2080 proof-tree. The function @{ML get_all_names} recursively selects all names. |
2080 proof-tree. The function @{ML get_all_names} recursively selects all names. |
2081 |
2081 |
2082 @{ML_response [display,gray] |
2082 @{ML_response [display,gray] |
2083 \<open>@{thm my_conjIa} |
2083 \<open>@{thm my_conjIa} |
2084 |> get_all_names |> sort string_ord\<close> |
2084 |> get_all_names |> sort string_ord\<close> |
2085 \<open>["", "HOL.All_def", "HOL.FalseE", "HOL.False_def", "HOL.TrueI", "HOL.True_def", |
2085 \<open>["", "HOL.All_def", "HOL.FalseE", "HOL.False_def", "HOL.TrueI", |
2086 "HOL.True_or_False", "HOL.allI", "HOL.and_def", "HOL.conjI", |
2086 "HOL.True_def", "HOL.True_or_False", "HOL.allI", "HOL.and_def", |
2087 "HOL.conjunct1", "HOL.conjunct2", "HOL.disjE", "HOL.eqTrueE", "HOL.eqTrueI", |
2087 "HOL.conjI", "HOL.conjunct1", "HOL.conjunct2", "HOL.disjE", |
2088 "HOL.ext", "HOL.fun_cong", "HOL.iffD1", "HOL.iffD2", "HOL.iffI", |
2088 "HOL.eqTrueE", "HOL.eqTrueI", "HOL.ext", "HOL.fun_cong", "HOL.iffD1", |
2089 "HOL.impI", "HOL.mp", "HOL.or_def", "HOL.refl", "HOL.rev_iffD1", |
2089 "HOL.iffD2", "HOL.iffI", "HOL.impI", "HOL.mp", "HOL.or_def", |
2090 "HOL.rev_iffD2", "HOL.spec", "HOL.ssubst", "HOL.subst", "HOL.sym", |
2090 "HOL.refl", "HOL.rev_iffD1", "HOL.rev_iffD2", "HOL.spec", |
|
2091 "HOL.ssubst", "HOL.subst", "HOL.sym", |
2091 "Pure.protectD", "Pure.protectI"]\<close>} |
2092 "Pure.protectD", "Pure.protectI"]\<close>} |
2092 |
2093 |
2093 The theorems @{thm [source] Pure.protectD} and @{thm [source] |
2094 The theorems @{thm [source] Pure.protectD} and @{thm [source] |
2094 Pure.protectI} that are internal theorems are always part of a |
2095 Pure.protectI} that are internal theorems are always part of a |
2095 proof in Isabelle. The other theorems are the theorems used in the proofs of the theorems |
2096 proof in Isabelle. The other theorems are the theorems used in the proofs of the theorems |
2110 are returned for @{thm [source] my_conjIc}. |
2111 are returned for @{thm [source] my_conjIc}. |
2111 |
2112 |
2112 @{ML_response [display,gray] |
2113 @{ML_response [display,gray] |
2113 \<open>@{thm my_conjIc} |
2114 \<open>@{thm my_conjIc} |
2114 |> get_all_names\<close> |
2115 |> get_all_names\<close> |
2115 \<open>["HOL.simp_thms_25", "Pure.conjunctionD1", "Pure.conjunctionD2", "Pure.conjunctionI", |
2116 \<open>["HOL.simp_thms_25", "Pure.conjunctionD1", "Pure.conjunctionD2", |
2116 "HOL.rev_mp", "HOL.exI", "HOL.allE", "HOL.exE",\<dots>]\<close>} |
2117 "Pure.conjunctionI", "HOL.rev_mp", "HOL.exI", "HOL.allE", |
|
2118 "HOL.exE",\<dots>]\<close>} |
2117 |
2119 |
2118 |
2120 |
2119 \begin{exercise} |
2121 \begin{exercise} |
2120 Have a look at the theorems that are used when a lemma is ``proved'' |
2122 Have a look at the theorems that are used when a lemma is ``proved'' |
2121 by \isacommand{sorry}? |
2123 by \isacommand{sorry}? |