| changeset 69605 | a96320074298 |
| parent 56798 | 939e88e79724 |
| 69604:d80b2df54d31 | 69605:a96320074298 |
|---|---|
6 |
6 |
7 theory K_R |
7 theory K_R |
8 imports RMD_Specification |
8 imports RMD_Specification |
9 begin |
9 begin |
10 |
10 |
11 spark_open "rmd/k_r" |
11 spark_open \<open>rmd/k_r\<close> |
12 |
12 |
13 spark_vc function_k_r_6 |
13 spark_vc function_k_r_6 |
14 using assms by (simp add: K'_def) |
14 using assms by (simp add: K'_def) |
15 |
15 |
16 spark_vc function_k_r_7 |
16 spark_vc function_k_r_7 |