lib/Tools/document
changeset 51822 7aebe43d6a14
parent 51081 70a4c11cd79e
child 52746 eec610972763
equal deleted inserted replaced
51821:8bbc5fd78cd2 51822:7aebe43d6a14
   108         *)
   108         *)
   109           echo "\\isakeeptag{${TAG}}"
   109           echo "\\isakeeptag{${TAG}}"
   110           ;;
   110           ;;
   111       esac
   111       esac
   112     done
   112     done
       
   113     echo
   113   ) > isabelletags.sty
   114   ) > isabelletags.sty
   114 }
   115 }
   115 
   116 
   116 
   117 
   117 # prepare document
   118 # prepare document