# HG changeset patch
# User wenzelm
# Date 1014318559 -3600
# Node ID d6a0d168291e4a8fcfe58fbd9e7682c66eef815d
# Parent  bca45be2d25b75f6a0aa48cb87bebb50876cf5b4
removed theory Option;

diff -r bca45be2d25b -r d6a0d168291e src/HOL/Bali/Basis.thy
--- a/src/HOL/Bali/Basis.thy	Thu Feb 21 20:08:09 2002 +0100
+++ b/src/HOL/Bali/Basis.thy	Thu Feb 21 20:09:19 2002 +0100
@@ -256,7 +256,7 @@
 (* e.g. lemmas is_stmt_rews = is_stmt_def [of "In1l x", simplified] *)
 
 translations
-  "option"<= (type) "Option.option"
+  "option"<= (type) "Datatype.option"
   "list"  <= (type) "List.list"
   "sum3"  <= (type) "Basis.sum3"
 
diff -r bca45be2d25b -r d6a0d168291e src/HOL/Bali/Eval.thy
--- a/src/HOL/Bali/Eval.thy	Thu Feb 21 20:08:09 2002 +0100
+++ b/src/HOL/Bali/Eval.thy	Thu Feb 21 20:09:19 2002 +0100
@@ -779,7 +779,7 @@
 
 ML {*
 local
-  fun is_None (Const ("Option.option.None",_)) = true
+  fun is_None (Const ("Datatype.option.None",_)) = true
     | is_None _ = false
   fun pred (t as (_ $ (Const ("Pair",_) $
      (Const ("Pair", _) $ x $ _) $ _ ) $ _)) = is_None x
@@ -806,7 +806,7 @@
 
 ML {*
 local
-  fun is_Some (Const ("Pair",_) $ (Const ("Option.option.Some",_) $ _)$ _) =true
+  fun is_Some (Const ("Pair",_) $ (Const ("Datatype.option.Some",_) $ _)$ _) =true
     | is_Some _ = false
   fun pred (_ $ (Const ("Pair",_) $
      _ $ (Const ("Pair", _) $ _ $ (Const ("Pair", _) $ _ $
diff -r bca45be2d25b -r d6a0d168291e src/HOL/Bali/Evaln.thy
--- a/src/HOL/Bali/Evaln.thy	Thu Feb 21 20:08:09 2002 +0100
+++ b/src/HOL/Bali/Evaln.thy	Thu Feb 21 20:09:19 2002 +0100
@@ -323,7 +323,7 @@
 
 ML {*
 local
-  fun is_Some (Const ("Pair",_) $ (Const ("Option.option.Some",_) $ _)$ _) =true
+  fun is_Some (Const ("Pair",_) $ (Const ("Datatype.option.Some",_) $ _)$ _) =true
     | is_Some _ = false
   fun pred (_ $ (Const ("Pair",_) $
      _ $ (Const ("Pair", _) $ _ $ (Const ("Pair", _) $ _ $
diff -r bca45be2d25b -r d6a0d168291e src/HOL/Map.thy
--- a/src/HOL/Map.thy	Thu Feb 21 20:08:09 2002 +0100
+++ b/src/HOL/Map.thy	Thu Feb 21 20:09:19 2002 +0100
@@ -6,7 +6,7 @@
 The datatype of `maps' (written ~=>); strongly resembles maps in VDM.
 *)
 
-Map = List + Option +
+Map = List +
 
 types ('a,'b) "~=>" = 'a => 'b option (infixr 0)
 
diff -r bca45be2d25b -r d6a0d168291e src/HOL/MiniML/Maybe.thy
--- a/src/HOL/MiniML/Maybe.thy	Thu Feb 21 20:08:09 2002 +0100
+++ b/src/HOL/MiniML/Maybe.thy	Thu Feb 21 20:09:19 2002 +0100
@@ -6,7 +6,7 @@
 Universal error monad.
 *)
 
-Maybe = Option + List +
+Maybe = Main +
 
 constdefs
   option_bind :: ['a option, 'a => 'b option] => 'b option
diff -r bca45be2d25b -r d6a0d168291e src/HOL/PreList.thy
--- a/src/HOL/PreList.thy	Thu Feb 21 20:08:09 2002 +0100
+++ b/src/HOL/PreList.thy	Thu Feb 21 20:09:19 2002 +0100
@@ -8,8 +8,7 @@
 *)
 
 theory PreList =
-  Option + Wellfounded_Relations + NatSimprocs + Recdef + Record +
-  Relation_Power:
+  Wellfounded_Relations + NatSimprocs + Recdef + Relation_Power:
 
 (*belongs to theory Divides*)
 declare dvdI [intro?]  dvdE [elim?]  dvd_trans [trans]
diff -r bca45be2d25b -r d6a0d168291e src/HOL/UNITY/Simple/Channel.thy
--- a/src/HOL/UNITY/Simple/Channel.thy	Thu Feb 21 20:08:09 2002 +0100
+++ b/src/HOL/UNITY/Simple/Channel.thy	Thu Feb 21 20:09:19 2002 +0100
@@ -8,7 +8,7 @@
 From Misra, "A Logic for Concurrent Programming" (1994), section 13.3
 *)
 
-Channel = WFair + Option + 
+Channel = WFair +
 
 types state = nat set
 
diff -r bca45be2d25b -r d6a0d168291e src/HOLCF/IOA/meta_theory/Automata.thy
--- a/src/HOLCF/IOA/meta_theory/Automata.thy	Thu Feb 21 20:08:09 2002 +0100
+++ b/src/HOLCF/IOA/meta_theory/Automata.thy	Thu Feb 21 20:09:19 2002 +0100
@@ -7,7 +7,7 @@
 *)   
 
 		       
-Automata = Option + Asig + Inductive +
+Automata = Asig +
 
 default type