160 "Rewrite","Rewrite'_Inst","Rewrite'_Set","Rewrite'_Set'_Inst", |
160 "Rewrite","Rewrite'_Inst","Rewrite'_Set","Rewrite'_Set'_Inst", |
161 "Substitute","Tac","Check'_elementswise", |
161 "Substitute","Tac","Check'_elementswise", |
162 "Take","Subproblem","Or'_to'_List"])); |
162 "Take","Subproblem","Or'_to'_List"])); |
163 |
163 |
164 val screxpr = Unsynchronized.ref (distinct (remove op = "" |
164 val screxpr = Unsynchronized.ref (distinct (remove op = "" |
165 ["HOL.Let","If","Repeat","While","Try","Or"])); |
165 ["Let","If","Repeat","While","Try","Or"])); |
166 |
166 |
167 val listfuns = Unsynchronized.ref [(*_all_ functions in Isa99.List.thy *) |
167 val listfuns = Unsynchronized.ref [(*_all_ functions in Isa99.List.thy *) |
168 "@","filter","concat","foldl","hd","last","set","list_all", |
168 "@","filter","concat","foldl","hd","last","set","list_all", |
169 "map","mem","nth","list_update","take","drop", |
169 "map","mem","nth","list_update","take","drop", |
170 "takeWhile","dropWhile","tl","butlast", |
170 "takeWhile","dropWhile","tl","butlast", |