--- a/src/HOL/ex/BinEx.thy Fri Sep 28 20:08:28 2001 +0200
+++ b/src/HOL/ex/BinEx.thy Fri Sep 28 20:09:10 2001 +0200
@@ -240,12 +240,12 @@
*}
consts normal :: "bin set"
-inductive "normal"
- intros [simp]
- Pls: "Pls: normal"
- Min: "Min: normal"
- BIT_F: "w: normal ==> w \<noteq> Pls ==> w BIT False : normal"
- BIT_T: "w: normal ==> w \<noteq> Min ==> w BIT True : normal"
+inductive normal
+ intros
+ Pls [simp]: "Pls: normal"
+ Min [simp]: "Min: normal"
+ BIT_F [simp]: "w: normal ==> w \<noteq> Pls ==> w BIT False : normal"
+ BIT_T [simp]: "w: normal ==> w \<noteq> Min ==> w BIT True : normal"
text {*
\medskip Binary arithmetic on normalized operands yields normalized