removed theory Option;
authorwenzelm
Thu Feb 21 20:09:19 2002 +0100 (2002-02-21)
changeset 12919d6a0d168291e
parent 12918 bca45be2d25b
child 12920 32292d83367b
removed theory Option;
src/HOL/Bali/Basis.thy
src/HOL/Bali/Eval.thy
src/HOL/Bali/Evaln.thy
src/HOL/Map.thy
src/HOL/MiniML/Maybe.thy
src/HOL/PreList.thy
src/HOL/UNITY/Simple/Channel.thy
src/HOLCF/IOA/meta_theory/Automata.thy
     1.1 --- a/src/HOL/Bali/Basis.thy	Thu Feb 21 20:08:09 2002 +0100
     1.2 +++ b/src/HOL/Bali/Basis.thy	Thu Feb 21 20:09:19 2002 +0100
     1.3 @@ -256,7 +256,7 @@
     1.4  (* e.g. lemmas is_stmt_rews = is_stmt_def [of "In1l x", simplified] *)
     1.5  
     1.6  translations
     1.7 -  "option"<= (type) "Option.option"
     1.8 +  "option"<= (type) "Datatype.option"
     1.9    "list"  <= (type) "List.list"
    1.10    "sum3"  <= (type) "Basis.sum3"
    1.11  
     2.1 --- a/src/HOL/Bali/Eval.thy	Thu Feb 21 20:08:09 2002 +0100
     2.2 +++ b/src/HOL/Bali/Eval.thy	Thu Feb 21 20:09:19 2002 +0100
     2.3 @@ -779,7 +779,7 @@
     2.4  
     2.5  ML {*
     2.6  local
     2.7 -  fun is_None (Const ("Option.option.None",_)) = true
     2.8 +  fun is_None (Const ("Datatype.option.None",_)) = true
     2.9      | is_None _ = false
    2.10    fun pred (t as (_ $ (Const ("Pair",_) $
    2.11       (Const ("Pair", _) $ x $ _) $ _ ) $ _)) = is_None x
    2.12 @@ -806,7 +806,7 @@
    2.13  
    2.14  ML {*
    2.15  local
    2.16 -  fun is_Some (Const ("Pair",_) $ (Const ("Option.option.Some",_) $ _)$ _) =true
    2.17 +  fun is_Some (Const ("Pair",_) $ (Const ("Datatype.option.Some",_) $ _)$ _) =true
    2.18      | is_Some _ = false
    2.19    fun pred (_ $ (Const ("Pair",_) $
    2.20       _ $ (Const ("Pair", _) $ _ $ (Const ("Pair", _) $ _ $
     3.1 --- a/src/HOL/Bali/Evaln.thy	Thu Feb 21 20:08:09 2002 +0100
     3.2 +++ b/src/HOL/Bali/Evaln.thy	Thu Feb 21 20:09:19 2002 +0100
     3.3 @@ -323,7 +323,7 @@
     3.4  
     3.5  ML {*
     3.6  local
     3.7 -  fun is_Some (Const ("Pair",_) $ (Const ("Option.option.Some",_) $ _)$ _) =true
     3.8 +  fun is_Some (Const ("Pair",_) $ (Const ("Datatype.option.Some",_) $ _)$ _) =true
     3.9      | is_Some _ = false
    3.10    fun pred (_ $ (Const ("Pair",_) $
    3.11       _ $ (Const ("Pair", _) $ _ $ (Const ("Pair", _) $ _ $
     4.1 --- a/src/HOL/Map.thy	Thu Feb 21 20:08:09 2002 +0100
     4.2 +++ b/src/HOL/Map.thy	Thu Feb 21 20:09:19 2002 +0100
     4.3 @@ -6,7 +6,7 @@
     4.4  The datatype of `maps' (written ~=>); strongly resembles maps in VDM.
     4.5  *)
     4.6  
     4.7 -Map = List + Option +
     4.8 +Map = List +
     4.9  
    4.10  types ('a,'b) "~=>" = 'a => 'b option (infixr 0)
    4.11  
     5.1 --- a/src/HOL/MiniML/Maybe.thy	Thu Feb 21 20:08:09 2002 +0100
     5.2 +++ b/src/HOL/MiniML/Maybe.thy	Thu Feb 21 20:09:19 2002 +0100
     5.3 @@ -6,7 +6,7 @@
     5.4  Universal error monad.
     5.5  *)
     5.6  
     5.7 -Maybe = Option + List +
     5.8 +Maybe = Main +
     5.9  
    5.10  constdefs
    5.11    option_bind :: ['a option, 'a => 'b option] => 'b option
     6.1 --- a/src/HOL/PreList.thy	Thu Feb 21 20:08:09 2002 +0100
     6.2 +++ b/src/HOL/PreList.thy	Thu Feb 21 20:09:19 2002 +0100
     6.3 @@ -8,8 +8,7 @@
     6.4  *)
     6.5  
     6.6  theory PreList =
     6.7 -  Option + Wellfounded_Relations + NatSimprocs + Recdef + Record +
     6.8 -  Relation_Power:
     6.9 +  Wellfounded_Relations + NatSimprocs + Recdef + Relation_Power:
    6.10  
    6.11  (*belongs to theory Divides*)
    6.12  declare dvdI [intro?]  dvdE [elim?]  dvd_trans [trans]
     7.1 --- a/src/HOL/UNITY/Simple/Channel.thy	Thu Feb 21 20:08:09 2002 +0100
     7.2 +++ b/src/HOL/UNITY/Simple/Channel.thy	Thu Feb 21 20:09:19 2002 +0100
     7.3 @@ -8,7 +8,7 @@
     7.4  From Misra, "A Logic for Concurrent Programming" (1994), section 13.3
     7.5  *)
     7.6  
     7.7 -Channel = WFair + Option + 
     7.8 +Channel = WFair +
     7.9  
    7.10  types state = nat set
    7.11  
     8.1 --- a/src/HOLCF/IOA/meta_theory/Automata.thy	Thu Feb 21 20:08:09 2002 +0100
     8.2 +++ b/src/HOLCF/IOA/meta_theory/Automata.thy	Thu Feb 21 20:09:19 2002 +0100
     8.3 @@ -7,7 +7,7 @@
     8.4  *)   
     8.5  
     8.6  		       
     8.7 -Automata = Option + Asig + Inductive +
     8.8 +Automata = Asig +
     8.9  
    8.10  default type
    8.11