abandoned theory Plain
authorhaftmann
Thu Feb 14 12:24:42 2013 +0100 (2013-02-14)
changeset 51112da97167e03f7
parent 51111 2e1bc14724b5
child 51113 222fb6cb2c3e
abandoned theory Plain
src/HOL/Big_Operators.thy
src/HOL/Code_Evaluation.thy
src/HOL/Equiv_Relations.thy
src/HOL/Int.thy
src/HOL/Lifting.thy
src/HOL/List.thy
src/HOL/Main.thy
src/HOL/Plain.thy
src/HOL/Predicate.thy
src/HOL/Quotient.thy
src/HOL/Record.thy
src/HOL/Transfer.thy
src/HOL/Typerep.thy
     1.1 --- a/src/HOL/Big_Operators.thy	Thu Feb 14 13:16:47 2013 +0100
     1.2 +++ b/src/HOL/Big_Operators.thy	Thu Feb 14 12:24:42 2013 +0100
     1.3 @@ -6,7 +6,7 @@
     1.4  header {* Big operators and finite (non-empty) sets *}
     1.5  
     1.6  theory Big_Operators
     1.7 -imports Plain
     1.8 +imports Finite_Set Metis
     1.9  begin
    1.10  
    1.11  subsection {* Generic monoid operation over a set *}
     2.1 --- a/src/HOL/Code_Evaluation.thy	Thu Feb 14 13:16:47 2013 +0100
     2.2 +++ b/src/HOL/Code_Evaluation.thy	Thu Feb 14 12:24:42 2013 +0100
     2.3 @@ -5,7 +5,7 @@
     2.4  header {* Term evaluation using the generic code generator *}
     2.5  
     2.6  theory Code_Evaluation
     2.7 -imports Plain Typerep New_DSequence
     2.8 +imports Typerep New_DSequence
     2.9  begin
    2.10  
    2.11  subsection {* Term representation *}
     3.1 --- a/src/HOL/Equiv_Relations.thy	Thu Feb 14 13:16:47 2013 +0100
     3.2 +++ b/src/HOL/Equiv_Relations.thy	Thu Feb 14 12:24:42 2013 +0100
     3.3 @@ -5,7 +5,7 @@
     3.4  header {* Equivalence Relations in Higher-Order Set Theory *}
     3.5  
     3.6  theory Equiv_Relations
     3.7 -imports Big_Operators Relation Plain
     3.8 +imports Big_Operators Relation
     3.9  begin
    3.10  
    3.11  subsection {* Equivalence relations -- set version *}
     4.1 --- a/src/HOL/Int.thy	Thu Feb 14 13:16:47 2013 +0100
     4.2 +++ b/src/HOL/Int.thy	Thu Feb 14 12:24:42 2013 +0100
     4.3 @@ -6,7 +6,7 @@
     4.4  header {* The Integers as Equivalence Classes over Pairs of Natural Numbers *} 
     4.5  
     4.6  theory Int
     4.7 -imports Equiv_Relations Wellfounded Quotient
     4.8 +imports Equiv_Relations Wellfounded Quotient FunDef
     4.9  begin
    4.10  
    4.11  subsection {* Definition of integers as a quotient type *}
     5.1 --- a/src/HOL/Lifting.thy	Thu Feb 14 13:16:47 2013 +0100
     5.2 +++ b/src/HOL/Lifting.thy	Thu Feb 14 12:24:42 2013 +0100
     5.3 @@ -6,7 +6,7 @@
     5.4  header {* Lifting package *}
     5.5  
     5.6  theory Lifting
     5.7 -imports Plain Equiv_Relations Transfer
     5.8 +imports Equiv_Relations Transfer
     5.9  keywords
    5.10    "print_quotmaps" "print_quotients" :: diag and
    5.11    "lift_definition" :: thy_goal and
     6.1 --- a/src/HOL/List.thy	Thu Feb 14 13:16:47 2013 +0100
     6.2 +++ b/src/HOL/List.thy	Thu Feb 14 12:24:42 2013 +0100
     6.3 @@ -5,7 +5,7 @@
     6.4  header {* The datatype of finite lists *}
     6.5  
     6.6  theory List
     6.7 -imports Plain Presburger Code_Numeral Quotient ATP
     6.8 +imports Presburger Code_Numeral Quotient ATP
     6.9  begin
    6.10  
    6.11  datatype 'a list =
     7.1 --- a/src/HOL/Main.thy	Thu Feb 14 13:16:47 2013 +0100
     7.2 +++ b/src/HOL/Main.thy	Thu Feb 14 12:24:42 2013 +0100
     7.3 @@ -1,7 +1,7 @@
     7.4  header {* Main HOL *}
     7.5  
     7.6  theory Main
     7.7 -imports Plain Predicate_Compile Nitpick
     7.8 +imports Predicate_Compile Nitpick Extraction
     7.9  begin
    7.10  
    7.11  text {*
    7.12 @@ -11,4 +11,18 @@
    7.13  
    7.14  text {* See further \cite{Nipkow-et-al:2002:tutorial} *}
    7.15  
    7.16 +no_notation
    7.17 +  bot ("\<bottom>") and
    7.18 +  top ("\<top>") and
    7.19 +  inf (infixl "\<sqinter>" 70) and
    7.20 +  sup (infixl "\<squnion>" 65) and
    7.21 +  Inf ("\<Sqinter>_" [900] 900) and
    7.22 +  Sup ("\<Squnion>_" [900] 900)
    7.23 +
    7.24 +no_syntax (xsymbols)
    7.25 +  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
    7.26 +  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
    7.27 +  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
    7.28 +  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
    7.29 +
    7.30  end
     8.1 --- a/src/HOL/Plain.thy	Thu Feb 14 13:16:47 2013 +0100
     8.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.3 @@ -1,26 +0,0 @@
     8.4 -header {* Plain HOL *}
     8.5 -
     8.6 -theory Plain
     8.7 -imports Datatype FunDef Extraction Metis Num
     8.8 -begin
     8.9 -
    8.10 -text {*
    8.11 -  Plain bootstrap of fundamental HOL tools and packages; does not
    8.12 -  include @{text Hilbert_Choice}.
    8.13 -*}
    8.14 -
    8.15 -no_notation
    8.16 -  bot ("\<bottom>") and
    8.17 -  top ("\<top>") and
    8.18 -  inf (infixl "\<sqinter>" 70) and
    8.19 -  sup (infixl "\<squnion>" 65) and
    8.20 -  Inf ("\<Sqinter>_" [900] 900) and
    8.21 -  Sup ("\<Squnion>_" [900] 900)
    8.22 -
    8.23 -no_syntax (xsymbols)
    8.24 -  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
    8.25 -  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
    8.26 -  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
    8.27 -  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
    8.28 -
    8.29 -end
     9.1 --- a/src/HOL/Predicate.thy	Thu Feb 14 13:16:47 2013 +0100
     9.2 +++ b/src/HOL/Predicate.thy	Thu Feb 14 12:24:42 2013 +0100
     9.3 @@ -8,20 +8,6 @@
     9.4  imports List
     9.5  begin
     9.6  
     9.7 -notation
     9.8 -  bot ("\<bottom>") and
     9.9 -  top ("\<top>") and
    9.10 -  inf (infixl "\<sqinter>" 70) and
    9.11 -  sup (infixl "\<squnion>" 65) and
    9.12 -  Inf ("\<Sqinter>_" [900] 900) and
    9.13 -  Sup ("\<Squnion>_" [900] 900)
    9.14 -
    9.15 -syntax (xsymbols)
    9.16 -  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
    9.17 -  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
    9.18 -  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
    9.19 -  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
    9.20 -
    9.21  subsection {* The type of predicate enumerations (a monad) *}
    9.22  
    9.23  datatype 'a pred = Pred "'a \<Rightarrow> bool"
    9.24 @@ -729,20 +715,8 @@
    9.25    by (simp add: pred_of_set_set_fold_sup ac_simps foldr_fold fun_eq_iff)
    9.26  
    9.27  no_notation
    9.28 -  bot ("\<bottom>") and
    9.29 -  top ("\<top>") and
    9.30 -  inf (infixl "\<sqinter>" 70) and
    9.31 -  sup (infixl "\<squnion>" 65) and
    9.32 -  Inf ("\<Sqinter>_" [900] 900) and
    9.33 -  Sup ("\<Squnion>_" [900] 900) and
    9.34    bind (infixl "\<guillemotright>=" 70)
    9.35  
    9.36 -no_syntax (xsymbols)
    9.37 -  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
    9.38 -  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
    9.39 -  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
    9.40 -  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
    9.41 -
    9.42  hide_type (open) pred seq
    9.43  hide_const (open) Pred eval single bind is_empty singleton if_pred not_pred holds
    9.44    Empty Insert Join Seq member pred_of_seq "apply" adjunct null the_only eq map not_unique the
    10.1 --- a/src/HOL/Quotient.thy	Thu Feb 14 13:16:47 2013 +0100
    10.2 +++ b/src/HOL/Quotient.thy	Thu Feb 14 12:24:42 2013 +0100
    10.3 @@ -5,7 +5,7 @@
    10.4  header {* Definition of Quotient Types *}
    10.5  
    10.6  theory Quotient
    10.7 -imports Plain Hilbert_Choice Equiv_Relations Lifting
    10.8 +imports Hilbert_Choice Equiv_Relations Lifting
    10.9  keywords
   10.10    "print_quotmapsQ3" "print_quotientsQ3" "print_quotconsts" :: diag and
   10.11    "quotient_type" :: thy_goal and "/" and
    11.1 --- a/src/HOL/Record.thy	Thu Feb 14 13:16:47 2013 +0100
    11.2 +++ b/src/HOL/Record.thy	Thu Feb 14 12:24:42 2013 +0100
    11.3 @@ -9,7 +9,7 @@
    11.4  header {* Extensible records with structural subtyping *}
    11.5  
    11.6  theory Record
    11.7 -imports Plain Quickcheck_Narrowing
    11.8 +imports Quickcheck_Narrowing
    11.9  keywords "record" :: thy_decl
   11.10  begin
   11.11  
    12.1 --- a/src/HOL/Transfer.thy	Thu Feb 14 13:16:47 2013 +0100
    12.2 +++ b/src/HOL/Transfer.thy	Thu Feb 14 12:24:42 2013 +0100
    12.3 @@ -5,7 +5,7 @@
    12.4  header {* Generic theorem transfer using relations *}
    12.5  
    12.6  theory Transfer
    12.7 -imports Plain Hilbert_Choice
    12.8 +imports Hilbert_Choice
    12.9  begin
   12.10  
   12.11  subsection {* Relator for function space *}
    13.1 --- a/src/HOL/Typerep.thy	Thu Feb 14 13:16:47 2013 +0100
    13.2 +++ b/src/HOL/Typerep.thy	Thu Feb 14 12:24:42 2013 +0100
    13.3 @@ -3,7 +3,7 @@
    13.4  header {* Reflecting Pure types into HOL *}
    13.5  
    13.6  theory Typerep
    13.7 -imports Plain String
    13.8 +imports String
    13.9  begin
   13.10  
   13.11  datatype typerep = Typerep String.literal "typerep list"