equal
deleted
inserted
replaced
9 |
9 |
10 theory Typedef_Nits |
10 theory Typedef_Nits |
11 imports Complex_Main |
11 imports Complex_Main |
12 begin |
12 begin |
13 |
13 |
14 nitpick_params [verbose, card = 1\<emdash>4, sat_solver = MiniSat_JNI, max_threads = 1, |
14 nitpick_params [verbose, card = 1\<emdash>4, sat_solver = Riss3g, max_threads = 1, |
15 timeout = 240] |
15 timeout = 240] |
16 |
16 |
17 definition "three = {0\<Colon>nat, 1, 2}" |
17 definition "three = {0\<Colon>nat, 1, 2}" |
18 typedef three = three |
18 typedef three = three |
19 unfolding three_def by blast |
19 unfolding three_def by blast |