tuned;
authorwenzelm
Thu Mar 30 21:26:10 2000 +0200 (2000-03-30)
changeset 862744ec33bb5c5b
parent 8626 76e3913ff421
child 8628 b3d9d8446473
tuned;
src/HOL/ex/Multiquote.thy
     1.1 --- a/src/HOL/ex/Multiquote.thy	Thu Mar 30 20:06:27 2000 +0200
     1.2 +++ b/src/HOL/ex/Multiquote.thy	Thu Mar 30 21:26:10 2000 +0200
     1.3 @@ -40,6 +40,6 @@
     1.4  term ".(.(` `x + `y).).";
     1.5  term ".(.(` `x + `y). o `f).";
     1.6  term ".(`(f o `g)).";
     1.7 -term ".(.(`(`(f o `g))).).";
     1.8 +term ".(.( ` `(f o `g) ).).";
     1.9  
    1.10  end;