33 "wet, quarter , quarter , quarter |- clean" |
33 "wet, quarter , quarter , quarter |- clean" |
34 |
34 |
35 |
35 |
36 (* "activate" definitions for use in proof *) |
36 (* "activate" definitions for use in proof *) |
37 |
37 |
38 ML_setup {* bind_thms ("changeI", [thm "context1"] RL ([thm "change"] RLN (2,[thm "cut"]))) *} |
38 ML {* bind_thms ("changeI", [thm "context1"] RL ([thm "change"] RLN (2,[thm "cut"]))) *} |
39 ML_setup {* bind_thms ("load1I", [thm "context1"] RL ([thm "load1"] RLN (2,[thm "cut"]))) *} |
39 ML {* bind_thms ("load1I", [thm "context1"] RL ([thm "load1"] RLN (2,[thm "cut"]))) *} |
40 ML_setup {* bind_thms ("washI", [thm "context1"] RL ([thm "wash"] RLN (2,[thm "cut"]))) *} |
40 ML {* bind_thms ("washI", [thm "context1"] RL ([thm "wash"] RLN (2,[thm "cut"]))) *} |
41 ML_setup {* bind_thms ("dryI", [thm "context1"] RL ([thm "dry"] RLN (2,[thm "cut"]))) *} |
41 ML {* bind_thms ("dryI", [thm "context1"] RL ([thm "dry"] RLN (2,[thm "cut"]))) *} |
42 |
42 |
43 (* a load of dirty clothes and two dollars gives you clean clothes *) |
43 (* a load of dirty clothes and two dollars gives you clean clothes *) |
44 |
44 |
45 lemma "dollar , dollar , dirty |- clean" |
45 lemma "dollar , dollar , dirty |- clean" |
46 apply (tactic {* best_tac (lazy_cs add_safes (thms "changeI" @ thms "load1I" @ thms "washI" @ thms "dryI")) 1 *}) |
46 apply (tactic {* best_tac (lazy_cs add_safes (thms "changeI" @ thms "load1I" @ thms "washI" @ thms "dryI")) 1 *}) |