src/Sequents/Washing.thy

--- a/src/Sequents/Washing.thy	Thu Feb 28 14:10:54 2013 +0100
+++ b/src/Sequents/Washing.thy	Thu Feb 28 14:22:14 2013 +0100
@@ -6,26 +6,25 @@
 imports ILL
 begin
 
-consts
-  dollar :: o
-  quarter :: o
-  loaded :: o
-  dirty :: o
-  wet :: o
+axiomatization
+  dollar :: o and
+  quarter :: o and
+  loaded :: o and
+  dirty :: o and
+  wet :: o and
   clean :: o
-
-axioms
+where
   change:
-  "dollar |- (quarter >< quarter >< quarter >< quarter)"
+  "dollar |- (quarter >< quarter >< quarter >< quarter)" and
 
   load1:
-  "quarter , quarter , quarter , quarter , quarter |- loaded"
+  "quarter , quarter , quarter , quarter , quarter |- loaded" and
 
   load2:
-  "dollar , quarter |- loaded"
+  "dollar , quarter |- loaded" and
 
   wash:
-  "loaded , dirty |- wet"
+  "loaded , dirty |- wet" and
 
   dry:
   "wet, quarter , quarter , quarter |- clean"