equal
deleted
inserted
replaced
45 |
45 |
46 \<close> ML \<open> (*//----------- build new fun XXXXX -------------------------------------------------\\*) |
46 \<close> ML \<open> (*//----------- build new fun XXXXX -------------------------------------------------\\*) |
47 (*//------------------ build new fun XXXXX -------------------------------------------------\\*) |
47 (*//------------------ build new fun XXXXX -------------------------------------------------\\*) |
48 (*\\------------------ build new fun XXXXX -------------------------------------------------//*) |
48 (*\\------------------ build new fun XXXXX -------------------------------------------------//*) |
49 \<close> ML \<open> (*\\----------- build new fun XXXXX -------------------------------------------------//*) |
49 \<close> ML \<open> (*\\----------- build new fun XXXXX -------------------------------------------------//*) |
50 \<close> ML \<open> |
|
51 \<close> |
50 \<close> |
52 ML \<open> |
51 ML \<open> |
53 \<close> ML \<open> |
52 \<close> ML \<open> |
54 \<close> ML \<open> |
53 \<close> ML \<open> |
55 \<close> |
54 \<close> |
65 ML_command \<open>Pretty.writeln prt\<close> |
64 ML_command \<open>Pretty.writeln prt\<close> |
66 declare [[ML_print_depth = 999]] |
65 declare [[ML_print_depth = 999]] |
67 declare [[ML_exception_trace]] |
66 declare [[ML_exception_trace]] |
68 \<close> |
67 \<close> |
69 |
68 |
70 section \<open>=================================================================\<close> |
69 section \<open>===================================================================================\<close> |
71 ML \<open> |
70 ML \<open> |
72 \<close> ML \<open> |
|
73 \<close> ML \<open> |
|
74 \<close> ML \<open> |
|
75 \<close> ML \<open> |
71 \<close> ML \<open> |
76 \<close> ML \<open> |
72 \<close> ML \<open> |
77 \<close> ML \<open> |
73 \<close> ML \<open> |
78 \<close> |
74 \<close> |
79 |
75 |
80 section \<open>=========="Minisubpbl/100-init-rootpbl.sml"========================================\<close> |
76 section \<open>===================================================================================\<close> |
81 ML \<open> |
77 ML \<open> |
82 \<close> ML \<open> |
|
83 \<close> ML \<open> |
|
84 \<close> ML \<open> |
|
85 \<close> ML \<open> |
78 \<close> ML \<open> |
86 \<close> ML \<open> |
79 \<close> ML \<open> |
87 \<close> ML \<open> |
80 \<close> ML \<open> |
88 \<close> |
81 \<close> |
89 |
82 |
90 section \<open>=================================================================\<close> |
83 section \<open>===================================================================================\<close> |
91 ML \<open> |
84 ML \<open> |
92 \<close> ML \<open> |
|
93 \<close> ML \<open> |
|
94 \<close> ML \<open> |
|
95 \<close> ML \<open> |
|
96 \<close> ML \<open> |
|
97 \<close> ML \<open> |
|
98 \<close> |
|
99 |
|
100 section \<open>=================================================================\<close> |
|
101 ML \<open> |
|
102 \<close> ML \<open> |
|
103 \<close> ML \<open> |
|
104 \<close> ML \<open> |
|
105 \<close> ML \<open> |
|
106 \<close> ML \<open> |
85 \<close> ML \<open> |
107 \<close> ML \<open> |
86 \<close> ML \<open> |
108 \<close> ML \<open> |
87 \<close> ML \<open> |
109 \<close> |
88 \<close> |
110 |
89 |