--- 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 *}
--- 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 *}
--- 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 *}
--- 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 *}
--- 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
--- 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 =
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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 *}
--- 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"