author haftmann Thu Feb 14 12:24:42 2013 +0100 (2013-02-14) changeset 51112 da97167e03f7 parent 51111 2e1bc14724b5 child 51113 222fb6cb2c3e
abandoned theory Plain
 src/HOL/Big_Operators.thy file | annotate | diff | revisions src/HOL/Code_Evaluation.thy file | annotate | diff | revisions src/HOL/Equiv_Relations.thy file | annotate | diff | revisions src/HOL/Int.thy file | annotate | diff | revisions src/HOL/Lifting.thy file | annotate | diff | revisions src/HOL/List.thy file | annotate | diff | revisions src/HOL/Main.thy file | annotate | diff | revisions src/HOL/Plain.thy file | annotate | diff | revisions src/HOL/Predicate.thy file | annotate | diff | revisions src/HOL/Quotient.thy file | annotate | diff | revisions src/HOL/Record.thy file | annotate | diff | revisions src/HOL/Transfer.thy file | annotate | diff | revisions src/HOL/Typerep.thy file | annotate | diff | revisions
```     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"
```