changeset 28838 | d5db6dfcb34a |
parent 28762 | f5d79aeffd81 |
child 29716 | b6266c4c68fe |
child 30240 | 5b25fee0362c |
28837:c6b17889237a | 28838:d5db6dfcb34a |
---|---|
12 use_thy "Inner_Syntax"; |
12 use_thy "Inner_Syntax"; |
13 use_thy "Misc"; |
13 use_thy "Misc"; |
14 use_thy "Generic"; |
14 use_thy "Generic"; |
15 use_thy "HOL_Specific"; |
15 use_thy "HOL_Specific"; |
16 use_thy "Quick_Reference"; |
16 use_thy "Quick_Reference"; |
17 use_thy "Symbols"; |
|
17 use_thy "ML_Tactic"; |
18 use_thy "ML_Tactic"; |