30 "wet, quarter , quarter , quarter |- clean" |
30 "wet, quarter , quarter , quarter |- clean" |
31 |
31 |
32 |
32 |
33 (* "activate" definitions for use in proof *) |
33 (* "activate" definitions for use in proof *) |
34 |
34 |
35 ML {* bind_thms ("changeI", [@{thm context1}] RL ([@{thm change}] RLN (2,[@{thm cut}]))) *} |
35 ML {* ML_Thms.bind_thms ("changeI", [@{thm context1}] RL ([@{thm change}] RLN (2,[@{thm cut}]))) *} |
36 ML {* bind_thms ("load1I", [@{thm context1}] RL ([@{thm load1}] RLN (2,[@{thm cut}]))) *} |
36 ML {* ML_Thms.bind_thms ("load1I", [@{thm context1}] RL ([@{thm load1}] RLN (2,[@{thm cut}]))) *} |
37 ML {* bind_thms ("washI", [@{thm context1}] RL ([@{thm wash}] RLN (2,[@{thm cut}]))) *} |
37 ML {* ML_Thms.bind_thms ("washI", [@{thm context1}] RL ([@{thm wash}] RLN (2,[@{thm cut}]))) *} |
38 ML {* bind_thms ("dryI", [@{thm context1}] RL ([@{thm dry}] RLN (2,[@{thm cut}]))) *} |
38 ML {* ML_Thms.bind_thms ("dryI", [@{thm context1}] RL ([@{thm dry}] RLN (2,[@{thm cut}]))) *} |
39 |
39 |
40 (* a load of dirty clothes and two dollars gives you clean clothes *) |
40 (* a load of dirty clothes and two dollars gives you clean clothes *) |
41 |
41 |
42 lemma "dollar , dollar , dirty |- clean" |
42 lemma "dollar , dollar , dirty |- clean" |
43 by (best add!: changeI load1I washI dryI) |
43 by (best add!: changeI load1I washI dryI) |