equal
deleted
inserted
replaced
7 val bin_chain = thm "bin_chain"; |
7 val bin_chain = thm "bin_chain"; |
8 val box_less = thm "box_less"; |
8 val box_less = thm "box_less"; |
9 val chain_def = thm "chain_def"; |
9 val chain_def = thm "chain_def"; |
10 val chainE = thm "chainE"; |
10 val chainE = thm "chainE"; |
11 val chainI = thm "chainI"; |
11 val chainI = thm "chainI"; |
|
12 val chain_const = thm "chain_const"; |
12 val chain_mono3 = thm "chain_mono3"; |
13 val chain_mono3 = thm "chain_mono3"; |
13 val chain_mono = thm "chain_mono"; |
14 val chain_mono = thm "chain_mono"; |
14 val chain_shift = thm "chain_shift"; |
15 val chain_shift = thm "chain_shift"; |
15 val chain_tord = thm "chain_tord"; |
16 val chain_tord = thm "chain_tord"; |
16 val finite_chain_def = thm "finite_chain_def"; |
17 val finite_chain_def = thm "finite_chain_def"; |