# HG changeset patch
# User paulson
# Date 912764573 -3600
# Node ID d1d5dd2f121cc466bd6c09082512dc7c6c6b9091
# Parent  bfd4923b0957a9c55efb614052f04fe0d32dfa9f
locales: assumes and defines may be empty

diff -r bfd4923b0957 -r d1d5dd2f121c src/HOL/Finite.thy
--- a/src/HOL/Finite.thy	Fri Dec 04 10:40:06 1998 +0100
+++ b/src/HOL/Finite.thy	Fri Dec 04 10:42:53 1998 +0100
@@ -63,8 +63,6 @@
     f    :: ['b,'a] => 'a
   assumes
     lcomm    "f x (f y z) = f y (f x z)"
-  defines
-    (*nothing*)
 
 locale ACe =
   fixes 
@@ -74,6 +72,5 @@
     ident    "f x e = x"
     commute  "f x y = f y x"
     assoc    "f (f x y) z = f x (f y z)"
-  defines
 
 end
diff -r bfd4923b0957 -r d1d5dd2f121c src/HOL/Induct/Multiset.thy
--- a/src/HOL/Induct/Multiset.thy	Fri Dec 04 10:40:06 1998 +0100
+++ b/src/HOL/Induct/Multiset.thy	Fri Dec 04 10:42:53 1998 +0100
@@ -49,8 +49,6 @@
     r :: "('a * 'a)set"
     W :: "'a multiset set"
 
-  assumes
-
   defines
     W_def       "W == acc(mult1 r)"
 end
diff -r bfd4923b0957 -r d1d5dd2f121c src/HOL/UNITY/Lift.thy
--- a/src/HOL/UNITY/Lift.thy	Fri Dec 04 10:40:06 1998 +0100
+++ b/src/HOL/UNITY/Lift.thy	Fri Dec 04 10:42:53 1998 +0100
@@ -160,6 +160,5 @@
   assumes
     Min_le_n    "Min <= n"
     n_le_Max    "n <= Max"
-  defines
 
 end
diff -r bfd4923b0957 -r d1d5dd2f121c src/Pure/Thy/thy_parse.ML
--- a/src/Pure/Thy/thy_parse.ML	Fri Dec 04 10:40:06 1998 +0100
+++ b/src/Pure/Thy/thy_parse.ML	Fri Dec 04 10:42:53 1998 +0100
@@ -425,9 +425,16 @@
 val locale_decl =
   (name --$$ "=") --
     ("fixes" $$--
-      (repeat (name --$$ "::" -- !! (typ -- opt_mixfix)) >> (mk_big_list o map mk_triple2))) --
-    ("assumes" $$-- (repeat ((ident >> quote) -- !! string) >> (mk_list o map mk_pair))) --
-    ("defines" $$-- (repeat ((ident >> quote) -- !! string) >> (mk_list o map mk_pair)))
+      (repeat (name --$$ "::" -- !! (typ -- opt_mixfix)) 
+       >> (mk_big_list o map mk_triple2))) --
+    (optional 
+     ("assumes" $$-- (repeat ((ident >> quote) -- !! string) 
+		     >> (mk_list o map mk_pair)))
+     "[]") --
+    (optional 
+     ("defines" $$-- (repeat ((ident >> quote) -- !! string) 
+		      >> (mk_list o map mk_pair)))
+     "[]")
   >> (fn (((nm, cs), asms), defs) => cat_lines [nm, cs, asms, defs]);
 
 
diff -r bfd4923b0957 -r d1d5dd2f121c src/ZF/AC/DC.thy
--- a/src/ZF/AC/DC.thy	Fri Dec 04 10:40:06 1998 +0100
+++ b/src/ZF/AC/DC.thy	Fri Dec 04 10:42:53 1998 +0100
@@ -52,8 +52,6 @@
     f	:: i
     allRR :: o
 
-  assumes
-
   defines
     XX_def    "XX == (UN n:nat.
 		      {f:succ(n)->domain(R). ALL k:n. <f`k, f`succ(k)> : R})"