src/HOL/HOL.thy
changeset 2393 651fce76c86c
parent 2372 a2999e19703b
child 2552 470bc495373e
     1.1 --- a/src/HOL/HOL.thy	Fri Dec 13 18:32:07 1996 +0100
     1.2 +++ b/src/HOL/HOL.thy	Fri Dec 13 18:40:50 1996 +0100
     1.3 @@ -174,9 +174,6 @@
     1.4    o_def         "(f::'b=>'c) o g == (%(x::'a). f(g(x)))"
     1.5    if_def        "If P x y == @z::'a. (P=True --> z=x) & (P=False --> z=y)"
     1.6  
     1.7 -(* start 8bit 1 *)
     1.8 -(* end 8bit 1 *)
     1.9 -
    1.10  end
    1.11  
    1.12  
    1.13 @@ -198,6 +195,3 @@
    1.14  
    1.15  val print_ast_translation =
    1.16    map alt_ast_tr' [("! ", "*All"), ("? ", "*Ex"), ("?! ", "*Ex1")];
    1.17 -
    1.18 -(* start 8bit 2 *)
    1.19 -(* end 8bit 2 *)