author  webertj 
Fri, 19 Oct 2012 15:12:52 +0200  
changeset 49962  a8cc904a6820 
parent 47108  2a1953f0d20d 
permissions  rwrr 
27368  1 
header {* Plain HOL *} 
2 

3 
theory Plain 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46691
diff
changeset

4 
imports Datatype FunDef Extraction Metis Num 
27368  5 
begin 
6 

29304  7 
text {* 
8 
Plain bootstrap of fundamental HOL tools and packages; does not 

9 
include @{text Hilbert_Choice}. 

10 
*} 

11 

46691  12 
no_notation 
13 
bot ("\<bottom>") and 

14 
top ("\<top>") and 

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

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

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

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

19 

20 
no_syntax (xsymbols) 

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

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

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

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

25 

27368  26 
end 