src/HOL/Main.thy
changeset 55579 207538943038
parent 55534 b18bdcbda41b
child 56048 d311c6377e08
     1.1 --- a/src/HOL/Main.thy	Wed Feb 19 10:21:02 2014 +0100
     1.2 +++ b/src/HOL/Main.thy	Wed Feb 19 10:30:21 2014 +0100
     1.3 @@ -1,7 +1,7 @@
     1.4  header {* Main HOL *}
     1.5  
     1.6  theory Main
     1.7 -imports Predicate_Compile Extraction Lifting_Sum List_Prefix Coinduction Nitpick BNF_GFP
     1.8 +imports Predicate_Compile Extraction Lifting_Sum Coinduction Nitpick BNF_GFP
     1.9  begin
    1.10  
    1.11  text {*
    1.12 @@ -32,7 +32,7 @@
    1.13    czero cinfinite cfinite csum cone ctwo Csum cprod cexp
    1.14    image2 image2p vimage2p Gr Grp collect fsts snds setl setr
    1.15    convol pick_middlep fstOp sndOp csquare inver relImage relInvImage
    1.16 -  prefCl PrefCl Succ Shift shift proj
    1.17 +  Succ Shift shift proj
    1.18  
    1.19  no_syntax (xsymbols)
    1.20    "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)