60 val {calc = scr_isa_fns, ...} = Specify.get_met (get_obj g_metID pt p') |
60 val {calc = scr_isa_fns, ...} = Specify.get_met (get_obj g_metID pt p') |
61 val opt = assoc (scr_isa_fns, scrop) |
61 val opt = assoc (scr_isa_fns, scrop) |
62 in |
62 in |
63 case opt of |
63 case opt of |
64 SOME isa_fn => ("OK", thy', isa_fn) |
64 SOME isa_fn => ("OK", thy', isa_fn) |
65 | NONE => ("applicable_in Calculate: unknown '" ^ scrop ^ "'", "", ("", Rule_Set.e_evalfn)) |
65 | NONE => ("applicable_in Calculate: unknown '" ^ scrop ^ "'", "", ("", Exec_Def.e_evalfn)) |
66 end |
66 end |
67 else |
67 else |
68 let |
68 let |
69 val thy' = get_obj g_domID pt (par_pblobj pt p); |
69 val thy' = get_obj g_domID pt (par_pblobj pt p); |
70 val (_, _,(*_,*)scr_isa_fns) = rew_info rls'(*rls*) |
70 val (_, _,(*_,*)scr_isa_fns) = rew_info rls'(*rls*) |
71 in |
71 in |
72 case assoc (scr_isa_fns, scrop) of |
72 case assoc (scr_isa_fns, scrop) of |
73 SOME isa_fn => ("OK",thy',isa_fn) |
73 SOME isa_fn => ("OK",thy',isa_fn) |
74 | NONE => ("applicable_in Calculate: unknown '" ^ scrop ^ "'", "", ("", Rule_Set.e_evalfn)) |
74 | NONE => ("applicable_in Calculate: unknown '" ^ scrop ^ "'", "", ("", Exec_Def.e_evalfn)) |
75 end |
75 end |
76 end; |
76 end; |
77 |
77 |
78 (*for Check_elementwise in applicable_in: [x=1,..] Assumptions -> (x,0<=x&..)*) |
78 (*for Check_elementwise in applicable_in: [x=1,..] Assumptions -> (x,0<=x&..)*) |
79 fun mk_set _(*thy*) _ _ (Const ("List.list.Nil", _)) _ = (Rule.e_term, []) |
79 fun mk_set _(*thy*) _ _ (Const ("List.list.Nil", _)) _ = (Rule.e_term, []) |