54 "~~~~~ fun partID, args:"; val (thy) = (ThyC.get_theory thy'); |
54 "~~~~~ fun partID, args:"; val (thy) = (ThyC.get_theory thy'); |
55 (*ERROR WAS: Theory loader: undefined entry for theory "Isac.Complex_Main"*) |
55 (*ERROR WAS: Theory loader: undefined entry for theory "Isac.Complex_Main"*) |
56 knowthys () |
56 knowthys () |
57 ; |
57 ; |
58 "~~~~~ fun knowthys , args:"; val () = (); |
58 "~~~~~ fun knowthys , args:"; val () = (); |
59 val allthys = filter_out (member Context.eq_thy |
59 val allthys = filter_out (Library.member Context.eq_thy |
60 [(*ThyC.get_theory "ProgLang",*) ThyC.get_theory "Interpret", |
60 [(*ThyC.get_theory "ProgLang",*) ThyC.get_theory "Interpret", |
61 ThyC.get_theory "MathEngine", ThyC.get_theory "BridgeLibisabelle"]) |
61 ThyC.get_theory "MathEngine", ThyC.get_theory "BridgeLibisabelle"]) |
62 (Theory.ancestors_of (ThyC.get_theory "Build_Thydata")); |
62 (Theory.ancestors_of (ThyC.get_theory "Build_Thydata")); |
63 length allthys = 152; (*in Isabelle2015/Isac*) |
63 length allthys = 152; (*in Isabelle2015/Isac*) |
64 (*ERROR WAS: Theory loader: undefined entry for theory "Isac.Complex_Main" |
64 (*ERROR WAS: Theory loader: undefined entry for theory "Isac.Complex_Main" |
123 interSteps 1 ([3,1], Res); |
123 interSteps 1 ([3,1], Res); |
124 val ((pt,_),_) = get_calc 1; show_pt pt; (* added [3,1,1] Frm + Res *) |
124 val ((pt,_),_) = get_calc 1; show_pt pt; (* added [3,1,1] Frm + Res *) |
125 |
125 |
126 val p = ([2,4], Res); |
126 val p = ([2,4], Res); |
127 "~~~~~ fun initContext, args:"; val ((cI:calcID), Thy_, (pos as (p,p_):pos')) = (1, Thy_, p); |
127 "~~~~~ fun initContext, args:"; val ((cI:calcID), Thy_, (pos as (p,p_):pos')) = (1, Thy_, p); |
128 member op = [Pbl,Met] p_ = false; |
128 Library.member op = [Pbl,Met] p_ = false; |
129 pos = ([],Res) = false; |
129 pos = ([],Res) = false; |
130 val cs as (ptp as (pt,_),_) = get_calc cI; |
130 val cs as (ptp as (pt,_),_) = get_calc cI; |
131 exist_lev_on' pt pos = true; |
131 exist_lev_on' pt pos = true; |
132 val pos' = lev_on' pt pos |
132 val pos' = lev_on' pt pos |
133 val tac = get_tac_checked pt pos'; |
133 val tac = get_tac_checked pt pos'; |
145 -rw-rw-r-- 1 wneuper wneuper 638 Aug 8 16:04 thy_isac_Test-thm-radd_left_commute.html*) |
145 -rw-rw-r-- 1 wneuper wneuper 638 Aug 8 16:04 thy_isac_Test-thm-radd_left_commute.html*) |
146 |
146 |
147 |
147 |
148 val p = ([3,1,1], Frm); |
148 val p = ([3,1,1], Frm); |
149 "~~~~~ fun initContext, args:"; val ((cI:calcID), Thy_, (pos as (p,p_):pos')) = (1, Thy_, p); |
149 "~~~~~ fun initContext, args:"; val ((cI:calcID), Thy_, (pos as (p,p_):pos')) = (1, Thy_, p); |
150 member op = [Pbl,Met] p_ = false; |
150 Library.member op = [Pbl,Met] p_ = false; |
151 pos = ([],Res) = false; |
151 pos = ([],Res) = false; |
152 val cs as (ptp as (pt,_),_) = get_calc cI; |
152 val cs as (ptp as (pt,_),_) = get_calc cI; |
153 exist_lev_on' pt pos = true; |
153 exist_lev_on' pt pos = true; |
154 val pos' = lev_on' pt pos |
154 val pos' = lev_on' pt pos |
155 val tac = get_tac_checked pt pos'; |
155 val tac = get_tac_checked pt pos'; |
167 -rw-rw-r-- 1 wneuper wneuper 646 Aug 8 16:04 thy_isac_Test-thm-risolate_bdv_add.html*) |
167 -rw-rw-r-- 1 wneuper wneuper 646 Aug 8 16:04 thy_isac_Test-thm-risolate_bdv_add.html*) |
168 |
168 |
169 |
169 |
170 val p = ([2,5], Res); |
170 val p = ([2,5], Res); |
171 "~~~~~ fun initContext, args:"; val ((cI:calcID), Thy_, (pos as (p,p_):pos')) = (1, Thy_, p); |
171 "~~~~~ fun initContext, args:"; val ((cI:calcID), Thy_, (pos as (p,p_):pos')) = (1, Thy_, p); |
172 member op = [Pbl,Met] p_ = false; |
172 Library.member op = [Pbl,Met] p_ = false; |
173 pos = ([],Res) = false; |
173 pos = ([],Res) = false; |
174 val cs as (ptp as (pt,_),_) = get_calc cI; |
174 val cs as (ptp as (pt,_),_) = get_calc cI; |
175 exist_lev_on' pt pos = true; |
175 exist_lev_on' pt pos = true; |
176 val pos' = lev_on' pt pos |
176 val pos' = lev_on' pt pos |
177 val tac = get_tac_checked pt pos'; |
177 val tac = get_tac_checked pt pos'; |
347 |
347 |
348 "----------- fun is_contained_in ------------------------"; |
348 "----------- fun is_contained_in ------------------------"; |
349 "----------- fun is_contained_in ------------------------"; |
349 "----------- fun is_contained_in ------------------------"; |
350 "----------- fun is_contained_in ------------------------"; |
350 "----------- fun is_contained_in ------------------------"; |
351 val r1 = Thm ("real_diff_minus",ThmC.numerals_to_Free @{thm real_diff_minus}); |
351 val r1 = Thm ("real_diff_minus",ThmC.numerals_to_Free @{thm real_diff_minus}); |
352 if Rtools.contains_rule r1 Test_simplify then () |
352 if Rule_Set.contains r1 Test_simplify then () |
353 else error "rewtools.sml Rtools.contains_rule Thm"; |
353 else error "rewtools.sml Rule_Set.contains Thm"; |
354 |
354 |
355 val r1 = Eval ("Groups.plus_class.plus", eval_binop "#add_"); |
355 val r1 = Eval ("Groups.plus_class.plus", eval_binop "#add_"); |
356 if Rtools.contains_rule r1 Test_simplify then () |
356 if Rule_Set.contains r1 Test_simplify then () |
357 else error "rewtools.sml Rtools.contains_rule Eval"; |
357 else error "rewtools.sml Rule_Set.contains Eval"; |
358 |
358 |
359 val r1 = Eval ("Groups.minus_class.minus", eval_binop "#add_"); |
359 val r1 = Eval ("Groups.minus_class.minus", eval_binop "#add_"); |
360 if not (Rtools.contains_rule r1 Test_simplify) then () |
360 if not (Rule_Set.contains r1 Test_simplify) then () |
361 else error "rewtools.sml Rtools.contains_rule Eval"; |
361 else error "rewtools.sml Rule_Set.contains Eval"; |