# HG changeset patch
# User haftmann
# Date 1360841082 -3600
# Node ID da97167e03f7b2ee7091e76bd2a0c8725d4d21c3
# Parent  2e1bc14724b5bd21f7a0cc06cca1db825212c2e0
abandoned theory Plain

diff -r 2e1bc14724b5 -r da97167e03f7 src/HOL/Big_Operators.thy
--- a/src/HOL/Big_Operators.thy	Thu Feb 14 13:16:47 2013 +0100
+++ b/src/HOL/Big_Operators.thy	Thu Feb 14 12:24:42 2013 +0100
@@ -6,7 +6,7 @@
 header {* Big operators and finite (non-empty) sets *}
 
 theory Big_Operators
-imports Plain
+imports Finite_Set Metis
 begin
 
 subsection {* Generic monoid operation over a set *}
diff -r 2e1bc14724b5 -r da97167e03f7 src/HOL/Code_Evaluation.thy
--- a/src/HOL/Code_Evaluation.thy	Thu Feb 14 13:16:47 2013 +0100
+++ b/src/HOL/Code_Evaluation.thy	Thu Feb 14 12:24:42 2013 +0100
@@ -5,7 +5,7 @@
 header {* Term evaluation using the generic code generator *}
 
 theory Code_Evaluation
-imports Plain Typerep New_DSequence
+imports Typerep New_DSequence
 begin
 
 subsection {* Term representation *}
diff -r 2e1bc14724b5 -r da97167e03f7 src/HOL/Equiv_Relations.thy
--- a/src/HOL/Equiv_Relations.thy	Thu Feb 14 13:16:47 2013 +0100
+++ b/src/HOL/Equiv_Relations.thy	Thu Feb 14 12:24:42 2013 +0100
@@ -5,7 +5,7 @@
 header {* Equivalence Relations in Higher-Order Set Theory *}
 
 theory Equiv_Relations
-imports Big_Operators Relation Plain
+imports Big_Operators Relation
 begin
 
 subsection {* Equivalence relations -- set version *}
diff -r 2e1bc14724b5 -r da97167e03f7 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Thu Feb 14 13:16:47 2013 +0100
+++ b/src/HOL/Int.thy	Thu Feb 14 12:24:42 2013 +0100
@@ -6,7 +6,7 @@
 header {* The Integers as Equivalence Classes over Pairs of Natural Numbers *} 
 
 theory Int
-imports Equiv_Relations Wellfounded Quotient
+imports Equiv_Relations Wellfounded Quotient FunDef
 begin
 
 subsection {* Definition of integers as a quotient type *}
diff -r 2e1bc14724b5 -r da97167e03f7 src/HOL/Lifting.thy
--- a/src/HOL/Lifting.thy	Thu Feb 14 13:16:47 2013 +0100
+++ b/src/HOL/Lifting.thy	Thu Feb 14 12:24:42 2013 +0100
@@ -6,7 +6,7 @@
 header {* Lifting package *}
 
 theory Lifting
-imports Plain Equiv_Relations Transfer
+imports Equiv_Relations Transfer
 keywords
   "print_quotmaps" "print_quotients" :: diag and
   "lift_definition" :: thy_goal and
diff -r 2e1bc14724b5 -r da97167e03f7 src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Feb 14 13:16:47 2013 +0100
+++ b/src/HOL/List.thy	Thu Feb 14 12:24:42 2013 +0100
@@ -5,7 +5,7 @@
 header {* The datatype of finite lists *}
 
 theory List
-imports Plain Presburger Code_Numeral Quotient ATP
+imports Presburger Code_Numeral Quotient ATP
 begin
 
 datatype 'a list =
diff -r 2e1bc14724b5 -r da97167e03f7 src/HOL/Main.thy
--- a/src/HOL/Main.thy	Thu Feb 14 13:16:47 2013 +0100
+++ b/src/HOL/Main.thy	Thu Feb 14 12:24:42 2013 +0100
@@ -1,7 +1,7 @@
 header {* Main HOL *}
 
 theory Main
-imports Plain Predicate_Compile Nitpick
+imports Predicate_Compile Nitpick Extraction
 begin
 
 text {*
@@ -11,4 +11,18 @@
 
 text {* See further \cite{Nipkow-et-al:2002:tutorial} *}
 
+no_notation
+  bot ("\<bottom>") and
+  top ("\<top>") and
+  inf (infixl "\<sqinter>" 70) and
+  sup (infixl "\<squnion>" 65) and
+  Inf ("\<Sqinter>_" [900] 900) and
+  Sup ("\<Squnion>_" [900] 900)
+
+no_syntax (xsymbols)
+  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
+  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
+  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
+  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
+
 end
diff -r 2e1bc14724b5 -r da97167e03f7 src/HOL/Plain.thy
--- a/src/HOL/Plain.thy	Thu Feb 14 13:16:47 2013 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,26 +0,0 @@
-header {* Plain HOL *}
-
-theory Plain
-imports Datatype FunDef Extraction Metis Num
-begin
-
-text {*
-  Plain bootstrap of fundamental HOL tools and packages; does not
-  include @{text Hilbert_Choice}.
-*}
-
-no_notation
-  bot ("\<bottom>") and
-  top ("\<top>") and
-  inf (infixl "\<sqinter>" 70) and
-  sup (infixl "\<squnion>" 65) and
-  Inf ("\<Sqinter>_" [900] 900) and
-  Sup ("\<Squnion>_" [900] 900)
-
-no_syntax (xsymbols)
-  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
-  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
-  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
-  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
-
-end
diff -r 2e1bc14724b5 -r da97167e03f7 src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Thu Feb 14 13:16:47 2013 +0100
+++ b/src/HOL/Predicate.thy	Thu Feb 14 12:24:42 2013 +0100
@@ -8,20 +8,6 @@
 imports List
 begin
 
-notation
-  bot ("\<bottom>") and
-  top ("\<top>") and
-  inf (infixl "\<sqinter>" 70) and
-  sup (infixl "\<squnion>" 65) and
-  Inf ("\<Sqinter>_" [900] 900) and
-  Sup ("\<Squnion>_" [900] 900)
-
-syntax (xsymbols)
-  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
-  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
-  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
-  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
-
 subsection {* The type of predicate enumerations (a monad) *}
 
 datatype 'a pred = Pred "'a \<Rightarrow> bool"
@@ -729,20 +715,8 @@
   by (simp add: pred_of_set_set_fold_sup ac_simps foldr_fold fun_eq_iff)
 
 no_notation
-  bot ("\<bottom>") and
-  top ("\<top>") and
-  inf (infixl "\<sqinter>" 70) and
-  sup (infixl "\<squnion>" 65) and
-  Inf ("\<Sqinter>_" [900] 900) and
-  Sup ("\<Squnion>_" [900] 900) and
   bind (infixl "\<guillemotright>=" 70)
 
-no_syntax (xsymbols)
-  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
-  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
-  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
-  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
-
 hide_type (open) pred seq
 hide_const (open) Pred eval single bind is_empty singleton if_pred not_pred holds
   Empty Insert Join Seq member pred_of_seq "apply" adjunct null the_only eq map not_unique the
diff -r 2e1bc14724b5 -r da97167e03f7 src/HOL/Quotient.thy
--- a/src/HOL/Quotient.thy	Thu Feb 14 13:16:47 2013 +0100
+++ b/src/HOL/Quotient.thy	Thu Feb 14 12:24:42 2013 +0100
@@ -5,7 +5,7 @@
 header {* Definition of Quotient Types *}
 
 theory Quotient
-imports Plain Hilbert_Choice Equiv_Relations Lifting
+imports Hilbert_Choice Equiv_Relations Lifting
 keywords
   "print_quotmapsQ3" "print_quotientsQ3" "print_quotconsts" :: diag and
   "quotient_type" :: thy_goal and "/" and
diff -r 2e1bc14724b5 -r da97167e03f7 src/HOL/Record.thy
--- a/src/HOL/Record.thy	Thu Feb 14 13:16:47 2013 +0100
+++ b/src/HOL/Record.thy	Thu Feb 14 12:24:42 2013 +0100
@@ -9,7 +9,7 @@
 header {* Extensible records with structural subtyping *}
 
 theory Record
-imports Plain Quickcheck_Narrowing
+imports Quickcheck_Narrowing
 keywords "record" :: thy_decl
 begin
 
diff -r 2e1bc14724b5 -r da97167e03f7 src/HOL/Transfer.thy
--- a/src/HOL/Transfer.thy	Thu Feb 14 13:16:47 2013 +0100
+++ b/src/HOL/Transfer.thy	Thu Feb 14 12:24:42 2013 +0100
@@ -5,7 +5,7 @@
 header {* Generic theorem transfer using relations *}
 
 theory Transfer
-imports Plain Hilbert_Choice
+imports Hilbert_Choice
 begin
 
 subsection {* Relator for function space *}
diff -r 2e1bc14724b5 -r da97167e03f7 src/HOL/Typerep.thy
--- a/src/HOL/Typerep.thy	Thu Feb 14 13:16:47 2013 +0100
+++ b/src/HOL/Typerep.thy	Thu Feb 14 12:24:42 2013 +0100
@@ -3,7 +3,7 @@
 header {* Reflecting Pure types into HOL *}
 
 theory Typerep
-imports Plain String
+imports String
 begin
 
 datatype typerep = Typerep String.literal "typerep list"