24 | is_ch [] (k::_) = false |
24 | is_ch [] (k::_) = false |
25 | is_ch (c::cs) (k::ks) = |
25 | is_ch (c::cs) (k::ks) = |
26 if c = k then is_ch cs ks else false |
26 if c = k then is_ch cs ks else false |
27 in is_ch (rev child) (rev key) end; |
27 in is_ch (rev child) (rev key) end; |
28 (* |
28 (* |
29 is_child_of ["root","univar","equation"] ["univar","equation"]; |
29 is_child_of ["root'","univar","equation"] ["univar","equation"]; |
30 val it = true : bool |
30 val it = true : bool |
31 is_child_of ["root","univar","equation"] ["system","equation"]; |
31 is_child_of ["root'","univar","equation"] ["system","equation"]; |
32 val it = false : bool |
32 val it = false : bool |
33 is_child_of ["equation"] ["system","equation"]; |
33 is_child_of ["equation"] ["system","equation"]; |
34 val it = false : bool |
34 val it = false : bool |
35 is_child_of ["root","univar","equation"] ["linear","univar","equation"]; |
35 is_child_of ["root'","univar","equation"] ["linear","univar","equation"]; |
36 val it = false : bool |
36 val it = false : bool |
37 *) |
37 *) |
38 |
38 |
39 (*.what tactics have to be hidden (in model/specify these may be several).*) |
39 (*.what tactics have to be hidden (in model/specify these may be several).*) |
40 datatype hid = |
40 datatype hid = |
73 :hide; |
73 :hide; |
74 is_hid [] "Rewrite" hide; |
74 is_hid [] "Rewrite" hide; |
75 val it = Show |
75 val it = Show |
76 is_hid ["any","problem"] "Refine_Tacitly" hide; |
76 is_hid ["any","problem"] "Refine_Tacitly" hide; |
77 val it = Htac |
77 val it = Htac |
78 is_hid ["root","univar","equation"] "Apply_Method" hide; |
78 is_hid ["root'","univar","equation"] "Apply_Method" hide; |
79 val it = Show |
79 val it = Show |
80 is_hid ["univar","equation"] "Apply_Method" hide; |
80 is_hid ["univar","equation"] "Apply_Method" hide; |
81 val it = Htac |
81 val it = Htac |
82 is_hid ["univar","equation"] "Specify_Problem" hide; |
82 is_hid ["univar","equation"] "Specify_Problem" hide; |
83 val it = Hspecify |
83 val it = Hspecify |
101 :hide; |
101 :hide; |
102 is_hide [] (Rewrite ("","")) hide; |
102 is_hide [] (Rewrite ("","")) hide; |
103 val it = Show |
103 val it = Show |
104 is_hide ["any","problem"] (Refine_Tacitly []) hide; |
104 is_hide ["any","problem"] (Refine_Tacitly []) hide; |
105 val it = Htac |
105 val it = Htac |
106 is_hide ["root","univar","equation"] (Apply_Method []) hide; |
106 is_hide ["root'","univar","equation"] (Apply_Method []) hide; |
107 val it = Show |
107 val it = Show |
108 is_hide ["univar","equation"] (Apply_Method []) hide; |
108 is_hide ["univar","equation"] (Apply_Method []) hide; |
109 val it = Htac |
109 val it = Htac |
110 is_hide ["univar","equation"] (Specify_Problem []) hide; |
110 is_hide ["univar","equation"] (Specify_Problem []) hide; |
111 val it = Hspecify |
111 val it = Hspecify |