author  kuncar 
Tue, 13 Aug 2013 15:59:22 +0200  
changeset 53012  cb82606b8215 
parent 51112  da97167e03f7 
child 54538  ba7392b52a7c 
permissions  rwrr 
12024  1 
header {* Main HOL *} 
2 

15131  3 
theory Main 
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
51112
diff
changeset

4 
imports Predicate_Compile Nitpick Extraction Lifting_Sum 
15131  5 
begin 
9650
6f0b89f2a1f9
Main now newstyle theory; added Main.ML for compatibility;
wenzelm
parents:
9619
diff
changeset

6 

29304  7 
text {* 
8 
Classical Higherorder Logic  only ``Main'', excluding real and 

9 
complex numbers etc. 

10 
*} 

11 

27367  12 
text {* See further \cite{Nipkowetal:2002:tutorial} *} 
25964  13 

51112  14 
no_notation 
15 
bot ("\<bottom>") and 

16 
top ("\<top>") and 

17 
inf (infixl "\<sqinter>" 70) and 

18 
sup (infixl "\<squnion>" 65) and 

19 
Inf ("\<Sqinter>_" [900] 900) and 

20 
Sup ("\<Squnion>_" [900] 900) 

21 

22 
no_syntax (xsymbols) 

23 
"_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_./ _)" [0, 10] 10) 

24 
"_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10) 

25 
"_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_./ _)" [0, 10] 10) 

26 
"_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10) 

27 

9650
6f0b89f2a1f9
Main now newstyle theory; added Main.ML for compatibility;
wenzelm
parents:
9619
diff
changeset

28 
end 