equal
deleted
inserted
replaced
8 ML_file "xmlsrc/thy-hierarchy.sml" |
8 ML_file "xmlsrc/thy-hierarchy.sml" |
9 |
9 |
10 CAUTION with testing *2file functions -- they are actually writing to ~/tmp |
10 CAUTION with testing *2file functions -- they are actually writing to ~/tmp |
11 *) |
11 *) |
12 |
12 |
13 val thy = @{theory "Isac"}; |
13 val thy = @{theory "Isac_Knowledge"}; |
14 |
14 |
15 "-----------------------------------------------------------------"; |
15 "-----------------------------------------------------------------"; |
16 "table of contents -----------------------------------------------"; |
16 "table of contents -----------------------------------------------"; |
17 "-----------------------------------------------------------------"; |
17 "-----------------------------------------------------------------"; |
18 "----------- fun thms_of -----------------------------------------"; |
18 "----------- fun thms_of -----------------------------------------"; |
182 :*) |
182 :*) |
183 |
183 |
184 "----------- fun revert_sym --------------------------------------"; |
184 "----------- fun revert_sym --------------------------------------"; |
185 "----------- fun revert_sym --------------------------------------"; |
185 "----------- fun revert_sym --------------------------------------"; |
186 "----------- fun revert_sym --------------------------------------"; |
186 "----------- fun revert_sym --------------------------------------"; |
187 val thy = @{theory Isac} |
187 val thy = @{theory Isac_Knowledge} |
188 val (Thm (thmID, thm)) = |
188 val (Thm (thmID, thm)) = |
189 revert_sym thy (Thm ("sym_real_mult_minus1", num_str (@{thm real_mult_minus1} RS @{thm sym}))) |
189 revert_sym thy (Thm ("sym_real_mult_minus1", num_str (@{thm real_mult_minus1} RS @{thm sym}))) |
190 ; |
190 ; |
191 if thmID = "Poly.real_mult_minus1" andalso string_of_thmI thm = "-1 * ?z = - ?z" |
191 if thmID = "Poly.real_mult_minus1" andalso string_of_thmI thm = "-1 * ?z = - ?z" |
192 then () else error "fun revert_sym changed 1"; |
192 then () else error "fun revert_sym changed 1"; |
208 (* |
208 (* |
209 if thmID = "real_mult_minus1" (* WAS "??.unknown" *) |
209 if thmID = "real_mult_minus1" (* WAS "??.unknown" *) |
210 then () else error "thms_of_rlss changed" |
210 then () else error "thms_of_rlss changed" |
211 *) |
211 *) |
212 ; |
212 ; |
213 "~~~~~ fun thms_of_rlss, args:"; val (thy, rlss) = (@{theory Isac}, rlss); |
213 "~~~~~ fun thms_of_rlss, args:"; val (thy, rlss) = (@{theory Isac_Knowledge}, rlss); |
214 val rlss' = (rlss : (rls' * (theory' * rls)) list) |
214 val rlss' = (rlss : (rls' * (theory' * rls)) list) |
215 |> map (thms_of_rls o #2 o #2) |
215 |> map (thms_of_rls o #2 o #2) |
216 (* = [[], [Thm ("real_diff_minus", "?a - ?b = ?a + -1 * ?b"), |
216 (* = [[], [Thm ("real_diff_minus", "?a - ?b = ?a + -1 * ?b"), |
217 Thm ("sym_real_mult_minus1", "- ?z1 = -1 * ?z1")]]*) |
217 Thm ("sym_real_mult_minus1", "- ?z1 = -1 * ?z1")]]*) |
218 |> flat |
218 |> flat |