|
1 (* lists of tactics, script-expressions etc. |
|
2 WN.14.3.00 |
|
3 *) |
|
4 |
|
5 theory' := overwritel (! theory', |
|
6 [(e_domID,Script.thy), |
|
7 ("Script.thy",Script.thy) |
|
8 ]); |
|
9 |
|
10 (*.record all theories defined for Scripts; in order to distinguish them |
|
11 from general IsacKnowledge defined later on.*) |
|
12 script_thys := !theory'; |
|
13 |
|
14 |
|
15 (*--vvv----- SHIFT? or delete ?*) |
|
16 val IDTyp = Type("Script.ID",[]); |
|
17 |
|
18 |
|
19 val tacs = ref (distinct |
|
20 ["Calculate", |
|
21 "Rewrite","Rewrite'_Inst","Rewrite'_Set","Rewrite'_Set'_Inst", |
|
22 "Substitute","Tac","Check'_elementswise", |
|
23 "Take","Subproblem","Or'_to'_List"] \ ""); |
|
24 |
|
25 val screxpr = ref (distinct |
|
26 ["Let","If","Repeat","While","Try","Or"] \ ""); |
|
27 |
|
28 val listfuns = ref [(*_all_ functions in Isa99.List.thy *) |
|
29 "@","filter","concat","foldl","hd","last","set","list_all", |
|
30 "map","mem","nth","list_update","take","drop", |
|
31 "takeWhile","dropWhile","tl","butlast", |
|
32 "rev","zip","upt","remdups","nodups","replicate", |
|
33 |
|
34 "Cons","Nil"]; |
|
35 |
|
36 val scrfuns = ref (distinct |
|
37 ["Testvar"] \ ""); |
|
38 |
|
39 val listexpr = ref ((!listfuns) union (!scrfuns)); |
|
40 |
|
41 val notsimp = ref |
|
42 (distinct (!tacs @ !screxpr @ (*!subpbls @*) !scrfuns @ !listfuns) \ ""); |
|
43 |
|
44 val negotiable = ref ((!tacs (*@ !subpbls*))); |
|
45 |
|
46 val tacpbl = ref |
|
47 (distinct (!tacs (*@ !subpbls*)) \ ""); |
|
48 (*--^^^----- SHIFT? or delete ?*) |
|
49 |
|
50 |
|
51 |
|
52 |
|
53 |
|
54 |
|
55 |
|
56 |
|
57 |
|
58 |