--- 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
--- 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
--- 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
--- 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]);
--- 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})"