--- a/src/Sequents/ILL/washing.thy Sun Sep 18 14:25:48 2005 +0200
+++ b/src/Sequents/ILL/washing.thy Sun Sep 18 15:20:08 2005 +0200
@@ -1,33 +1,38 @@
-
-(* code by Sara Kalvala, based on Paulson's LK
+(* $Id$ *)
+
+(* code by Sara Kalvala, based on Paulson's LK
and Moore's tisl.ML *)
-washing = ILL +
+theory washing
+imports ILL
+begin
consts
-
-dollar,quarter,loaded,dirty,wet,clean :: "o"
+ dollar :: o
+ quarter :: o
+ loaded :: o
+ dirty :: o
+ wet :: o
+ clean :: o
-
-rules
-
-
- change
+axioms
+ change:
"dollar |- (quarter >< quarter >< quarter >< quarter)"
- load1
+ load1:
"quarter , quarter , quarter , quarter , quarter |- loaded"
- load2
+ load2:
"dollar , quarter |- loaded"
- wash
+ wash:
"loaded , dirty |- wet"
- dry
+ dry:
"wet, quarter , quarter , quarter |- clean"
+ML {* use_legacy_bindings (the_context ()) *}
+
end
-
\ No newline at end of file